:: by Micha{\l} Muzalewski and Wojciech Skaba

::

:: Received October 13, 1990

:: Copyright (c) 1990-2011 Association of Mizar Users

begin

Lm1: for X1, X2 being set st X1 <> {} & X2 <> {} holds

for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]

proof end;

Lm2: for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds

for x being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]

proof end;

Lm3: for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds

for x being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]

proof end;

theorem :: MCART_2:1

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y holds

Y1 misses X ) )

proof end;

theorem Th2: :: MCART_2:2

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y holds

Y1 misses X ) )

proof end;

definition

let x1, x2, x3, x4, x5 be set ;

func [x1,x2,x3,x4,x5] -> set equals :: MCART_2:def 1

[[x1,x2,x3,x4],x5];

correctness

coherence

[[x1,x2,x3,x4],x5] is set ;

;

end;
func [x1,x2,x3,x4,x5] -> set equals :: MCART_2:def 1

[[x1,x2,x3,x4],x5];

correctness

coherence

[[x1,x2,x3,x4],x5] is set ;

;

:: deftheorem defines [ MCART_2:def 1 :

for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5];

theorem Th3: :: MCART_2:3

proof end;

theorem :: MCART_2:4

proof end;

theorem Th6: :: MCART_2:5

proof end;

theorem Th7: :: MCART_2:6

for x1, x2, x3, x4, x5, y1, y2, y3, y4, y5 being set st [x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 )

proof end;

theorem Th8: :: MCART_2:7

for X being set st X <> {} holds

ex x being set st

( x in X & ( for x1, x2, x3, x4, x5 being set holds

( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] ) ) )

ex x being set st

( x in X & ( for x1, x2, x3, x4, x5 being set holds

( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] ) ) )

proof end;

definition

let X1, X2, X3, X4, X5 be set ;

func [:X1,X2,X3,X4,X5:] -> set equals :: MCART_2:def 2

[:[:X1,X2,X3,X4:],X5:];

correctness

coherence

[:[:X1,X2,X3,X4:],X5:] is set ;

;

end;
func [:X1,X2,X3,X4,X5:] -> set equals :: MCART_2:def 2

[:[:X1,X2,X3,X4:],X5:];

correctness

coherence

[:[:X1,X2,X3,X4:],X5:] is set ;

;

:: deftheorem defines [: MCART_2:def 2 :

for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:];

theorem Th9: :: MCART_2:8

proof end;

theorem :: MCART_2:9

proof end;

theorem Th12: :: MCART_2:10

proof end;

theorem Th13: :: MCART_2:11

for X1, X2, X3, X4, X5 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) iff [:X1,X2,X3,X4,X5:] <> {} )

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) iff [:X1,X2,X3,X4,X5:] <> {} )

proof end;

theorem Th14: :: MCART_2:12

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 )

proof end;

theorem :: MCART_2:13

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st [:X1,X2,X3,X4,X5:] <> {} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 )

proof end;

theorem :: MCART_2:14

proof end;

theorem Th17: :: MCART_2:15

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]

for x being Element of [:X1,X2,X3,X4,X5:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5]

proof end;

definition

let X1, X2, X3, X4, X5 be set ;

assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5:];

func x `1 -> Element of X1 means :Def3: :: MCART_2:def 3

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x1;

existence

ex b_{1} being Element of X1 st

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x1 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x2 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x3 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x4;

existence

ex b_{1} being Element of X4 st

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x4

for b_{1}, b_{2} being Element of X4 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x4 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{2} = x4 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x5;

existence

ex b_{1} being Element of X5 st

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x5

for b_{1}, b_{2} being Element of X5 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{1} = x5 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b_{2} = x5 ) holds

b_{1} = b_{2}

end;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5:];

func x `1 -> Element of X1 means :Def3: :: MCART_2:def 3

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x1;

existence

ex b

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def4: :: MCART_2:def 4for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x2;

existence

ex b

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def5: :: MCART_2:def 5for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x3;

existence

ex b

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `4 -> Element of X4 means :Def6: :: MCART_2:def 6for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x4;

existence

ex b

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `5 -> Element of X5 means :Def7: :: MCART_2:def 7for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

it = x5;

existence

ex b

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines `1 MCART_2:def 3 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for b

( b

b

:: deftheorem Def4 defines `2 MCART_2:def 4 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for b

( b

b

:: deftheorem Def5 defines `3 MCART_2:def 5 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for b

( b

b

:: deftheorem Def6 defines `4 MCART_2:def 6 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for b

( b

b

:: deftheorem Def7 defines `5 MCART_2:def 7 :

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for b

( b

b

theorem :: MCART_2:16

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 ) by Def3, Def4, Def5, Def6, Def7;

for x being Element of [:X1,X2,X3,X4,X5:]

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 ) by Def3, Def4, Def5, Def6, Def7;

theorem Th19: :: MCART_2:17

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5)]

for x being Element of [:X1,X2,X3,X4,X5:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5)]

proof end;

theorem Th20: :: MCART_2:18

for X1, X2, X3, X4, X5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:] holds

( x `1 = (((x `1) `1) `1) `1 & x `2 = (((x `1) `1) `1) `2 & x `3 = ((x `1) `1) `2 & x `4 = (x `1) `2 & x `5 = x `2 )

for x being Element of [:X1,X2,X3,X4,X5:] holds

( x `1 = (((x `1) `1) `1) `1 & x `2 = (((x `1) `1) `1) `2 & x `3 = ((x `1) `1) `2 & x `4 = (x `1) `2 & x `5 = x `2 )

proof end;

theorem Th21: :: MCART_2:19

for X1, X2, X3, X4, X5 being set st ( X1 c= [:X1,X2,X3,X4,X5:] or X1 c= [:X2,X3,X4,X5,X1:] or X1 c= [:X3,X4,X5,X1,X2:] or X1 c= [:X4,X5,X1,X2,X3:] or X1 c= [:X5,X1,X2,X3,X4:] ) holds

X1 = {}

X1 = {}

proof end;

theorem :: MCART_2:20

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st [:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 )

proof end;

theorem Th23: :: MCART_2:21

proof end;

theorem :: MCART_2:22

for X1, X2, X3, X4, X5 being set

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 ) by Def3, Def4, Def5, Def6, Def7;

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} holds

for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 ) by Def3, Def4, Def5, Def6, Def7;

theorem :: MCART_2:23

for y1, X1, X2, X3, X4, X5 being set

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y1 = xx1 ) holds

y1 = x `1

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y1 = xx1 ) holds

y1 = x `1

proof end;

theorem :: MCART_2:24

for y2, X1, X2, X3, X4, X5 being set

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y2 = xx2 ) holds

y2 = x `2

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y2 = xx2 ) holds

y2 = x `2

proof end;

theorem :: MCART_2:25

for y3, X1, X2, X3, X4, X5 being set

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y3 = xx3 ) holds

y3 = x `3

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y3 = xx3 ) holds

y3 = x `3

proof end;

theorem :: MCART_2:26

for y4, X1, X2, X3, X4, X5 being set

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y4 = xx4 ) holds

y4 = x `4

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y4 = xx4 ) holds

y4 = x `4

proof end;

theorem :: MCART_2:27

for y5, X1, X2, X3, X4, X5 being set

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y5 = xx5 ) holds

y5 = x `5

for x being Element of [:X1,X2,X3,X4,X5:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5 st x = [xx1,xx2,xx3,xx4,xx5] holds

y5 = xx5 ) holds

y5 = x `5

proof end;

theorem Th30: :: MCART_2:28

for y, X1, X2, X3, X4, X5 being set st y in [:X1,X2,X3,X4,X5:] holds

ex x1, x2, x3, x4, x5 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] )

ex x1, x2, x3, x4, x5 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] )

proof end;

theorem Th31: :: MCART_2:29

for x1, x2, x3, x4, x5, X1, X2, X3, X4, X5 being set holds

( [x1,x2,x3,x4,x5] in [:X1,X2,X3,X4,X5:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 ) )

( [x1,x2,x3,x4,x5] in [:X1,X2,X3,X4,X5:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 ) )

proof end;

theorem :: MCART_2:30

for X1, X2, X3, X4, X5, Z being set st ( for y being set holds

( y in Z iff ex x1, x2, x3, x4, x5 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] ) ) ) holds

Z = [:X1,X2,X3,X4,X5:]

( y in Z iff ex x1, x2, x3, x4, x5 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & y = [x1,x2,x3,x4,x5] ) ) ) holds

Z = [:X1,X2,X3,X4,X5:]

proof end;

theorem Th33: :: MCART_2:31

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 )

for x being Element of [:X1,X2,X3,X4,X5:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 )

proof end;

theorem :: MCART_2:32

for X1, X2, X3, X4, X5 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for x being Element of [:X1,X2,X3,X4,X5:] st x in [:A1,A2,A3,A4,A5:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 )

proof end;

theorem Th35: :: MCART_2:33

for X1, X2, X3, X4, X5, Y1, Y2, Y3, Y4, Y5 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 holds

[:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:]

[:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:]

proof end;

definition

let X1, X2, X3, X4, X5 be set ;

let A1 be Subset of X1;

let A2 be Subset of X2;

let A3 be Subset of X3;

let A4 be Subset of X4;

let A5 be Subset of X5;

:: original: [:

redefine func [:A1,A2,A3,A4,A5:] -> Subset of [:X1,X2,X3,X4,X5:];

coherence

[:A1,A2,A3,A4,A5:] is Subset of [:X1,X2,X3,X4,X5:] by Th35;

end;
let A1 be Subset of X1;

let A2 be Subset of X2;

let A3 be Subset of X3;

let A4 be Subset of X4;

let A5 be Subset of X5;

:: original: [:

redefine func [:A1,A2,A3,A4,A5:] -> Subset of [:X1,X2,X3,X4,X5:];

coherence

[:A1,A2,A3,A4,A5:] is Subset of [:X1,X2,X3,X4,X5:] by Th35;

theorem :: MCART_2:34

for X1, X2 being set st X1 <> {} & X2 <> {} holds

for xx being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st xx = [xx1,xx2] by Lm1;

for xx being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st xx = [xx1,xx2] by Lm1;

theorem :: MCART_2:35

for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds

for xx being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st xx = [xx1,xx2,xx3] by Lm2;

for xx being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st xx = [xx1,xx2,xx3] by Lm2;

theorem :: MCART_2:36

for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds

for xx being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st xx = [xx1,xx2,xx3,xx4] by Lm3;

for xx being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st xx = [xx1,xx2,xx3,xx4] by Lm3;

begin

theorem :: MCART_2:37

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y holds

Y1 misses X ) )

proof end;

theorem Th40: :: MCART_2:38

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in Y holds

Y1 misses X ) )

proof end;

definition

let x1, x2, x3, x4, x5, x6 be set ;

func [x1,x2,x3,x4,x5,x6] -> set equals :: MCART_2:def 8

[[x1,x2,x3,x4,x5],x6];

correctness

coherence

[[x1,x2,x3,x4,x5],x6] is set ;

;

end;
func [x1,x2,x3,x4,x5,x6] -> set equals :: MCART_2:def 8

[[x1,x2,x3,x4,x5],x6];

correctness

coherence

[[x1,x2,x3,x4,x5],x6] is set ;

;

:: deftheorem defines [ MCART_2:def 8 :

for x1, x2, x3, x4, x5, x6 being set holds [x1,x2,x3,x4,x5,x6] = [[x1,x2,x3,x4,x5],x6];

theorem Th41: :: MCART_2:39

proof end;

theorem :: MCART_2:40

for x1, x2, x3, x4, x5, x6 being set holds [x1,x2,x3,x4,x5,x6] = [[x1,x2,x3,x4],x5,x6] by MCART_1:def 3;

theorem :: MCART_2:41

proof end;

theorem :: MCART_2:42

theorem Th45: :: MCART_2:43

for x1, x2, x3, x4, x5, x6, y1, y2, y3, y4, y5, y6 being set st [x1,x2,x3,x4,x5,x6] = [y1,y2,y3,y4,y5,y6] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 )

proof end;

theorem Th46: :: MCART_2:44

for X being set st X <> {} holds

ex v being set st

( v in X & ( for x1, x2, x3, x4, x5, x6 being set holds

( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4,x5,x6] ) ) )

ex v being set st

( v in X & ( for x1, x2, x3, x4, x5, x6 being set holds

( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4,x5,x6] ) ) )

proof end;

definition

let X1, X2, X3, X4, X5, X6 be set ;

func [:X1,X2,X3,X4,X5,X6:] -> set equals :: MCART_2:def 9

[:[:X1,X2,X3,X4,X5:],X6:];

coherence

[:[:X1,X2,X3,X4,X5:],X6:] is set ;

end;
func [:X1,X2,X3,X4,X5,X6:] -> set equals :: MCART_2:def 9

[:[:X1,X2,X3,X4,X5:],X6:];

coherence

[:[:X1,X2,X3,X4,X5:],X6:] is set ;

:: deftheorem defines [: MCART_2:def 9 :

for X1, X2, X3, X4, X5, X6 being set holds [:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3,X4,X5:],X6:];

theorem Th47: :: MCART_2:45

for X1, X2, X3, X4, X5, X6 being set holds [:X1,X2,X3,X4,X5,X6:] = [:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:]

proof end;

theorem :: MCART_2:46

for X1, X2, X3, X4, X5, X6 being set holds [:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3,X4:],X5,X6:] by ZFMISC_1:def 3;

theorem :: MCART_2:47

proof end;

theorem :: MCART_2:48

for X1, X2, X3, X4, X5, X6 being set holds [:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2:],X3,X4,X5,X6:] by Th12;

theorem Th51: :: MCART_2:49

for X1, X2, X3, X4, X5, X6 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} ) iff [:X1,X2,X3,X4,X5,X6:] <> {} )

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} ) iff [:X1,X2,X3,X4,X5,X6:] <> {} )

proof end;

theorem Th52: :: MCART_2:50

for X1, X2, X3, X4, X5, X6, Y1, Y2, Y3, Y4, Y5, Y6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & [:X1,X2,X3,X4,X5,X6:] = [:Y1,Y2,Y3,Y4,Y5,Y6:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 )

proof end;

theorem :: MCART_2:51

for X1, X2, X3, X4, X5, X6, Y1, Y2, Y3, Y4, Y5, Y6 being set st [:X1,X2,X3,X4,X5,X6:] <> {} & [:X1,X2,X3,X4,X5,X6:] = [:Y1,Y2,Y3,Y4,Y5,Y6:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 )

proof end;

theorem :: MCART_2:52

proof end;

theorem Th55: :: MCART_2:53

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6]

for x being Element of [:X1,X2,X3,X4,X5,X6:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6]

proof end;

definition

let X1, X2, X3, X4, X5, X6 be set ;

assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6:];

func x `1 -> Element of X1 means :Def10: :: MCART_2:def 10

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x1;

existence

ex b_{1} being Element of X1 st

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x1 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x2 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x3 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x4;

existence

ex b_{1} being Element of X4 st

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x4

for b_{1}, b_{2} being Element of X4 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x4 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{2} = x4 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x5;

existence

ex b_{1} being Element of X5 st

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x5

for b_{1}, b_{2} being Element of X5 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x5 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{2} = x5 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x6;

existence

ex b_{1} being Element of X6 st

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x6

for b_{1}, b_{2} being Element of X6 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{1} = x6 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b_{2} = x6 ) holds

b_{1} = b_{2}

end;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6:];

func x `1 -> Element of X1 means :Def10: :: MCART_2:def 10

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x1;

existence

ex b

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def11: :: MCART_2:def 11for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x2;

existence

ex b

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def12: :: MCART_2:def 12for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x3;

existence

ex b

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `4 -> Element of X4 means :Def13: :: MCART_2:def 13for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x4;

existence

ex b

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `5 -> Element of X5 means :Def14: :: MCART_2:def 14for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x5;

existence

ex b

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `6 -> Element of X6 means :Def15: :: MCART_2:def 15for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

it = x6;

existence

ex b

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines `1 MCART_2:def 10 :

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for b

( b

b

:: deftheorem Def11 defines `2 MCART_2:def 11 :

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for b

( b

b

:: deftheorem Def12 defines `3 MCART_2:def 12 :

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for b

( b

b

:: deftheorem Def13 defines `4 MCART_2:def 13 :

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for b

( b

b

:: deftheorem Def14 defines `5 MCART_2:def 14 :

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for b

( b

b

:: deftheorem Def15 defines `6 MCART_2:def 15 :

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for b

( b

b

theorem :: MCART_2:54

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 ) by Def10, Def11, Def12, Def13, Def14, Def15;

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 ) by Def10, Def11, Def12, Def13, Def14, Def15;

theorem Th57: :: MCART_2:55

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6)]

for x being Element of [:X1,X2,X3,X4,X5,X6:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6)]

proof end;

theorem Th58: :: MCART_2:56

for X1, X2, X3, X4, X5, X6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:] holds

( x `1 = ((((x `1) `1) `1) `1) `1 & x `2 = ((((x `1) `1) `1) `1) `2 & x `3 = (((x `1) `1) `1) `2 & x `4 = ((x `1) `1) `2 & x `5 = (x `1) `2 & x `6 = x `2 )

for x being Element of [:X1,X2,X3,X4,X5,X6:] holds

( x `1 = ((((x `1) `1) `1) `1) `1 & x `2 = ((((x `1) `1) `1) `1) `2 & x `3 = (((x `1) `1) `1) `2 & x `4 = ((x `1) `1) `2 & x `5 = (x `1) `2 & x `6 = x `2 )

proof end;

theorem Th59: :: MCART_2:57

for X1, X2, X3, X4, X5, X6 being set st ( X1 c= [:X1,X2,X3,X4,X5,X6:] or X1 c= [:X2,X3,X4,X5,X6,X1:] or X1 c= [:X3,X4,X5,X6,X1,X2:] or X1 c= [:X4,X5,X6,X1,X2,X3:] or X1 c= [:X5,X6,X1,X2,X3,X4:] or X1 c= [:X6,X1,X2,X3,X4,X5:] ) holds

X1 = {}

X1 = {}

proof end;

theorem :: MCART_2:58

for X1, X2, X3, X4, X5, X6, Y1, Y2, Y3, Y4, Y5, Y6 being set st [:X1,X2,X3,X4,X5,X6:] meets [:Y1,Y2,Y3,Y4,Y5,Y6:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 )

proof end;

theorem Th61: :: MCART_2:59

for x1, x2, x3, x4, x5, x6 being set holds [:{x1},{x2},{x3},{x4},{x5},{x6}:] = {[x1,x2,x3,x4,x5,x6]}

proof end;

theorem :: MCART_2:60

for X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 ) by Def10, Def11, Def12, Def13, Def14, Def15;

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} holds

for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 ) by Def10, Def11, Def12, Def13, Def14, Def15;

theorem :: MCART_2:61

for y1, X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y1 = xx1 ) holds

y1 = x `1

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y1 = xx1 ) holds

y1 = x `1

proof end;

theorem :: MCART_2:62

for y2, X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y2 = xx2 ) holds

y2 = x `2

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y2 = xx2 ) holds

y2 = x `2

proof end;

theorem :: MCART_2:63

for y3, X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y3 = xx3 ) holds

y3 = x `3

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y3 = xx3 ) holds

y3 = x `3

proof end;

theorem :: MCART_2:64

for y4, X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y4 = xx4 ) holds

y4 = x `4

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y4 = xx4 ) holds

y4 = x `4

proof end;

theorem :: MCART_2:65

for y5, X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y5 = xx5 ) holds

y5 = x `5

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y5 = xx5 ) holds

y5 = x `5

proof end;

theorem :: MCART_2:66

for y6, X1, X2, X3, X4, X5, X6 being set

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y6 = xx6 ) holds

y6 = x `6

for x being Element of [:X1,X2,X3,X4,X5,X6:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6 st x = [xx1,xx2,xx3,xx4,xx5,xx6] holds

y6 = xx6 ) holds

y6 = x `6

proof end;

theorem Th69: :: MCART_2:67

for z, X1, X2, X3, X4, X5, X6 being set st z in [:X1,X2,X3,X4,X5,X6:] holds

ex x1, x2, x3, x4, x5, x6 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & z = [x1,x2,x3,x4,x5,x6] )

ex x1, x2, x3, x4, x5, x6 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & z = [x1,x2,x3,x4,x5,x6] )

proof end;

theorem Th70: :: MCART_2:68

for x1, x2, x3, x4, x5, x6, X1, X2, X3, X4, X5, X6 being set holds

( [x1,x2,x3,x4,x5,x6] in [:X1,X2,X3,X4,X5,X6:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 ) )

( [x1,x2,x3,x4,x5,x6] in [:X1,X2,X3,X4,X5,X6:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 ) )

proof end;

theorem :: MCART_2:69

for X1, X2, X3, X4, X5, X6, Z being set st ( for z being set holds

( z in Z iff ex x1, x2, x3, x4, x5, x6 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & z = [x1,x2,x3,x4,x5,x6] ) ) ) holds

Z = [:X1,X2,X3,X4,X5,X6:]

( z in Z iff ex x1, x2, x3, x4, x5, x6 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & z = [x1,x2,x3,x4,x5,x6] ) ) ) holds

Z = [:X1,X2,X3,X4,X5,X6:]

proof end;

theorem Th72: :: MCART_2:70

for X1, X2, X3, X4, X5, X6, Y1, Y2, Y3, Y4, Y5, Y6 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} & Y6 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 )

for x being Element of [:X1,X2,X3,X4,X5,X6:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 )

proof end;

theorem :: MCART_2:71

for X1, X2, X3, X4, X5, X6 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for x being Element of [:X1,X2,X3,X4,X5,X6:] st x in [:A1,A2,A3,A4,A5,A6:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 )

proof end;

theorem Th74: :: MCART_2:72

for X1, X2, X3, X4, X5, X6, Y1, Y2, Y3, Y4, Y5, Y6 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 holds

[:X1,X2,X3,X4,X5,X6:] c= [:Y1,Y2,Y3,Y4,Y5,Y6:]

[:X1,X2,X3,X4,X5,X6:] c= [:Y1,Y2,Y3,Y4,Y5,Y6:]

proof end;

theorem :: MCART_2:73

for X1, X2, X3, X4, X5, X6 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6 holds [:A1,A2,A3,A4,A5,A6:] is Subset of [:X1,X2,X3,X4,X5,X6:] by Th74;

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6 holds [:A1,A2,A3,A4,A5,A6:] is Subset of [:X1,X2,X3,X4,X5,X6:] by Th74;

begin

theorem :: MCART_2:74

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in Y holds

Y1 misses X ) )

proof end;

theorem Th77: :: MCART_2:75

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in Y holds

Y1 misses X ) )

proof end;

definition

let x1, x2, x3, x4, x5, x6, x7 be set ;

func [x1,x2,x3,x4,x5,x6,x7] -> set equals :: MCART_2:def 16

[[x1,x2,x3,x4,x5,x6],x7];

correctness

coherence

[[x1,x2,x3,x4,x5,x6],x7] is set ;

;

end;
func [x1,x2,x3,x4,x5,x6,x7] -> set equals :: MCART_2:def 16

[[x1,x2,x3,x4,x5,x6],x7];

correctness

coherence

[[x1,x2,x3,x4,x5,x6],x7] is set ;

;

:: deftheorem defines [ MCART_2:def 16 :

for x1, x2, x3, x4, x5, x6, x7 being set holds [x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3,x4,x5,x6],x7];

theorem Th78: :: MCART_2:76

for x1, x2, x3, x4, x5, x6, x7 being set holds [x1,x2,x3,x4,x5,x6,x7] = [[[[[[x1,x2],x3],x4],x5],x6],x7]

proof end;

theorem :: MCART_2:77

for x1, x2, x3, x4, x5, x6, x7 being set holds [x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3,x4,x5],x6,x7] by MCART_1:def 3;

theorem :: MCART_2:78

for x1, x2, x3, x4, x5, x6, x7 being set holds [x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3,x4],x5,x6,x7] by MCART_1:27;

theorem :: MCART_2:79

proof end;

theorem :: MCART_2:80

for x1, x2, x3, x4, x5, x6, x7 being set holds [x1,x2,x3,x4,x5,x6,x7] = [[x1,x2],x3,x4,x5,x6,x7] by Th6;

theorem Th83: :: MCART_2:81

for x1, x2, x3, x4, x5, x6, x7, y1, y2, y3, y4, y5, y6, y7 being set st [x1,x2,x3,x4,x5,x6,x7] = [y1,y2,y3,y4,y5,y6,y7] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 )

proof end;

theorem Th84: :: MCART_2:82

for X being set st X <> {} holds

ex x being set st

( x in X & ( for x1, x2, x3, x4, x5, x6, x7 being set holds

( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5,x6,x7] ) ) )

ex x being set st

( x in X & ( for x1, x2, x3, x4, x5, x6, x7 being set holds

( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5,x6,x7] ) ) )

proof end;

definition

let X1, X2, X3, X4, X5, X6, X7 be set ;

func [:X1,X2,X3,X4,X5,X6,X7:] -> set equals :: MCART_2:def 17

[:[:X1,X2,X3,X4,X5,X6:],X7:];

correctness

coherence

[:[:X1,X2,X3,X4,X5,X6:],X7:] is set ;

;

end;
func [:X1,X2,X3,X4,X5,X6,X7:] -> set equals :: MCART_2:def 17

[:[:X1,X2,X3,X4,X5,X6:],X7:];

correctness

coherence

[:[:X1,X2,X3,X4,X5,X6:],X7:] is set ;

;

:: deftheorem defines [: MCART_2:def 17 :

for X1, X2, X3, X4, X5, X6, X7 being set holds [:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4,X5,X6:],X7:];

theorem Th85: :: MCART_2:83

for X1, X2, X3, X4, X5, X6, X7 being set holds [:X1,X2,X3,X4,X5,X6,X7:] = [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:]

proof end;

theorem :: MCART_2:84

for X1, X2, X3, X4, X5, X6, X7 being set holds [:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4,X5:],X6,X7:] by ZFMISC_1:def 3;

theorem :: MCART_2:85

for X1, X2, X3, X4, X5, X6, X7 being set holds [:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4:],X5,X6,X7:] by MCART_1:49;

theorem :: MCART_2:86

for X1, X2, X3, X4, X5, X6, X7 being set holds [:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3:],X4,X5,X6,X7:]

proof end;

theorem :: MCART_2:87

for X1, X2, X3, X4, X5, X6, X7 being set holds [:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2:],X3,X4,X5,X6,X7:] by Th12;

theorem Th90: :: MCART_2:88

for X1, X2, X3, X4, X5, X6, X7 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7:] <> {} )

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7:] <> {} )

proof end;

theorem Th91: :: MCART_2:89

for X1, X2, X3, X4, X5, X6, X7, Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & [:X1,X2,X3,X4,X5,X6,X7:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 )

proof end;

theorem :: MCART_2:90

for X1, X2, X3, X4, X5, X6, X7, Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st [:X1,X2,X3,X4,X5,X6,X7:] <> {} & [:X1,X2,X3,X4,X5,X6,X7:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 )

proof end;

theorem :: MCART_2:91

proof end;

theorem Th94: :: MCART_2:92

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7]

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7]

proof end;

definition

let X1, X2, X3, X4, X5, X6, X7 be set ;

assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6,X7:];

func x `1 -> Element of X1 means :Def18: :: MCART_2:def 18

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x1;

existence

ex b_{1} being Element of X1 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x4;

existence

ex b_{1} being Element of X4 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x4

for b_{1}, b_{2} being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x4 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x5;

existence

ex b_{1} being Element of X5 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x5

for b_{1}, b_{2} being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x5 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x6;

existence

ex b_{1} being Element of X6 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x6

for b_{1}, b_{2} being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x6 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x7;

existence

ex b_{1} being Element of X7 st

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x7

for b_{1}, b_{2} being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{1} = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b_{2} = x7 ) holds

b_{1} = b_{2}

end;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6,X7:];

func x `1 -> Element of X1 means :Def18: :: MCART_2:def 18

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x1;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def19: :: MCART_2:def 19for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x2;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def20: :: MCART_2:def 20for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x3;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `4 -> Element of X4 means :Def21: :: MCART_2:def 21for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x4;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `5 -> Element of X5 means :Def22: :: MCART_2:def 22for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x5;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `6 -> Element of X6 means :Def23: :: MCART_2:def 23for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x6;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `7 -> Element of X7 means :Def24: :: MCART_2:def 24for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

it = x7;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines `1 MCART_2:def 18 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

:: deftheorem Def19 defines `2 MCART_2:def 19 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

:: deftheorem Def20 defines `3 MCART_2:def 20 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

:: deftheorem Def21 defines `4 MCART_2:def 21 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

:: deftheorem Def22 defines `5 MCART_2:def 22 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

:: deftheorem Def23 defines `6 MCART_2:def 23 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

:: deftheorem Def24 defines `7 MCART_2:def 24 :

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for b

( b

b

theorem :: MCART_2:93

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 ) by Def18, Def19, Def20, Def21, Def22, Def23, Def24;

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 ) by Def18, Def19, Def20, Def21, Def22, Def23, Def24;

theorem Th96: :: MCART_2:94

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7)]

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7)]

proof end;

theorem Th97: :: MCART_2:95

for X1, X2, X3, X4, X5, X6, X7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] holds

( x `1 = (((((x `1) `1) `1) `1) `1) `1 & x `2 = (((((x `1) `1) `1) `1) `1) `2 & x `3 = ((((x `1) `1) `1) `1) `2 & x `4 = (((x `1) `1) `1) `2 & x `5 = ((x `1) `1) `2 & x `6 = (x `1) `2 & x `7 = x `2 )

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] holds

( x `1 = (((((x `1) `1) `1) `1) `1) `1 & x `2 = (((((x `1) `1) `1) `1) `1) `2 & x `3 = ((((x `1) `1) `1) `1) `2 & x `4 = (((x `1) `1) `1) `2 & x `5 = ((x `1) `1) `2 & x `6 = (x `1) `2 & x `7 = x `2 )

proof end;

theorem Th98: :: MCART_2:96

for X1, X2, X3, X4, X5, X6, X7 being set st ( X1 c= [:X1,X2,X3,X4,X5,X6,X7:] or X1 c= [:X2,X3,X4,X5,X6,X7,X1:] or X1 c= [:X3,X4,X5,X6,X7,X1,X2:] or X1 c= [:X4,X5,X6,X7,X1,X2,X3:] or X1 c= [:X5,X6,X7,X1,X2,X3,X4:] or X1 c= [:X6,X7,X1,X2,X3,X4,X5:] or X1 c= [:X7,X1,X2,X3,X4,X5,X6:] ) holds

X1 = {}

X1 = {}

proof end;

theorem Th99: :: MCART_2:97

for X1, X2, X3, X4, X5, X6, X7, Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st [:X1,X2,X3,X4,X5,X6,X7:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 )

proof end;

theorem Th100: :: MCART_2:98

for x1, x2, x3, x4, x5, x6, x7 being set holds [:{x1},{x2},{x3},{x4},{x5},{x6},{x7}:] = {[x1,x2,x3,x4,x5,x6,x7]}

proof end;

theorem :: MCART_2:99

for X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 ) by Def18, Def19, Def20, Def21, Def22, Def23, Def24;

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} holds

for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 ) by Def18, Def19, Def20, Def21, Def22, Def23, Def24;

theorem :: MCART_2:100

for y1, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y1 = xx1 ) holds

y1 = x `1

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y1 = xx1 ) holds

y1 = x `1

proof end;

theorem :: MCART_2:101

for y2, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y2 = xx2 ) holds

y2 = x `2

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y2 = xx2 ) holds

y2 = x `2

proof end;

theorem :: MCART_2:102

for y3, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y3 = xx3 ) holds

y3 = x `3

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y3 = xx3 ) holds

y3 = x `3

proof end;

theorem :: MCART_2:103

for y4, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y4 = xx4 ) holds

y4 = x `4

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y4 = xx4 ) holds

y4 = x `4

proof end;

theorem :: MCART_2:104

for y5, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y5 = xx5 ) holds

y5 = x `5

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y5 = xx5 ) holds

y5 = x `5

proof end;

theorem :: MCART_2:105

for y6, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y6 = xx6 ) holds

y6 = x `6

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y6 = xx6 ) holds

y6 = x `6

proof end;

theorem :: MCART_2:106

for y7, X1, X2, X3, X4, X5, X6, X7 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y7 = xx7 ) holds

y7 = x `7

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds

y7 = xx7 ) holds

y7 = x `7

proof end;

theorem Th109: :: MCART_2:107

for y, X1, X2, X3, X4, X5, X6, X7 being set st y in [:X1,X2,X3,X4,X5,X6,X7:] holds

ex x1, x2, x3, x4, x5, x6, x7 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & y = [x1,x2,x3,x4,x5,x6,x7] )

ex x1, x2, x3, x4, x5, x6, x7 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & y = [x1,x2,x3,x4,x5,x6,x7] )

proof end;

theorem Th110: :: MCART_2:108

for x1, x2, x3, x4, x5, x6, x7, X1, X2, X3, X4, X5, X6, X7 being set holds

( [x1,x2,x3,x4,x5,x6,x7] in [:X1,X2,X3,X4,X5,X6,X7:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 ) )

( [x1,x2,x3,x4,x5,x6,x7] in [:X1,X2,X3,X4,X5,X6,X7:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 ) )

proof end;

theorem :: MCART_2:109

for X1, X2, X3, X4, X5, X6, X7, Z being set st ( for y being set holds

( y in Z iff ex x1, x2, x3, x4, x5, x6, x7 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & y = [x1,x2,x3,x4,x5,x6,x7] ) ) ) holds

Z = [:X1,X2,X3,X4,X5,X6,X7:]

( y in Z iff ex x1, x2, x3, x4, x5, x6, x7 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & y = [x1,x2,x3,x4,x5,x6,x7] ) ) ) holds

Z = [:X1,X2,X3,X4,X5,X6,X7:]

proof end;

theorem Th112: :: MCART_2:110

for X1, X2, X3, X4, X5, X6, X7, Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} & Y6 <> {} & Y7 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 )

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 )

proof end;

theorem :: MCART_2:111

for X1, X2, X3, X4, X5, X6, X7 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st x in [:A1,A2,A3,A4,A5,A6,A7:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 )

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7

for x being Element of [:X1,X2,X3,X4,X5,X6,X7:] st x in [:A1,A2,A3,A4,A5,A6,A7:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 )

proof end;

theorem Th114: :: MCART_2:112

for X1, X2, X3, X4, X5, X6, X7, Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7 holds

[:X1,X2,X3,X4,X5,X6,X7:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:]

[:X1,X2,X3,X4,X5,X6,X7:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:]

proof end;

theorem :: MCART_2:113

for X1, X2, X3, X4, X5, X6, X7 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7 holds [:A1,A2,A3,A4,A5,A6,A7:] is Subset of [:X1,X2,X3,X4,X5,X6,X7:] by Th114;

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7 holds [:A1,A2,A3,A4,A5,A6,A7:] is Subset of [:X1,X2,X3,X4,X5,X6,X7:] by Th114;

begin

theorem :: MCART_2:114

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in Y holds

Y1 misses X ) )

proof end;

theorem Th117: :: MCART_2:115

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in Y holds

Y1 misses X ) )

proof end;

definition

let x1, x2, x3, x4, x5, x6, x7, x8 be set ;

func [x1,x2,x3,x4,x5,x6,x7,x8] -> set equals :: MCART_2:def 25

[[x1,x2,x3,x4,x5,x6,x7],x8];

correctness

coherence

[[x1,x2,x3,x4,x5,x6,x7],x8] is set ;

;

end;
func [x1,x2,x3,x4,x5,x6,x7,x8] -> set equals :: MCART_2:def 25

[[x1,x2,x3,x4,x5,x6,x7],x8];

correctness

coherence

[[x1,x2,x3,x4,x5,x6,x7],x8] is set ;

;

:: deftheorem defines [ MCART_2:def 25 :

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6,x7],x8];

theorem :: MCART_2:116

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8]

proof end;

theorem :: MCART_2:117

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6],x7,x8] by MCART_1:def 3;

theorem :: MCART_2:118

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5],x6,x7,x8] by MCART_1:27;

theorem :: MCART_2:119

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4],x5,x6,x7,x8] by Th3;

theorem :: MCART_2:120

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3],x4,x5,x6,x7,x8]

proof end;

theorem :: MCART_2:121

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2],x3,x4,x5,x6,x7,x8] by Th6;

theorem Th124: :: MCART_2:122

for x1, x2, x3, x4, x5, x6, x7, x8, y1, y2, y3, y4, y5, y6, y7, y8 being set st [x1,x2,x3,x4,x5,x6,x7,x8] = [y1,y2,y3,y4,y5,y6,y7,y8] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 & x8 = y8 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 & x8 = y8 )

proof end;

theorem Th125: :: MCART_2:123

for X being set st X <> {} holds

ex y being set st

( y in X & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set holds

( ( not x1 in X & not x2 in X ) or not y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) )

ex y being set st

( y in X & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set holds

( ( not x1 in X & not x2 in X ) or not y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) )

proof end;

definition

let X1, X2, X3, X4, X5, X6, X7, X8 be set ;

func [:X1,X2,X3,X4,X5,X6,X7,X8:] -> set equals :: MCART_2:def 26

[:[:X1,X2,X3,X4,X5,X6,X7:],X8:];

correctness

coherence

[:[:X1,X2,X3,X4,X5,X6,X7:],X8:] is set ;

;

end;
func [:X1,X2,X3,X4,X5,X6,X7,X8:] -> set equals :: MCART_2:def 26

[:[:X1,X2,X3,X4,X5,X6,X7:],X8:];

correctness

coherence

[:[:X1,X2,X3,X4,X5,X6,X7:],X8:] is set ;

;

:: deftheorem defines [: MCART_2:def 26 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8:];

theorem Th126: :: MCART_2:124

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:]

proof end;

theorem :: MCART_2:125

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6:],X7,X8:] by ZFMISC_1:def 3;

theorem :: MCART_2:126

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5:],X6,X7,X8:] by MCART_1:49;

theorem :: MCART_2:127

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8:] by Th9;

theorem :: MCART_2:128

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8:]

proof end;

theorem :: MCART_2:129

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8:] by Th12;

theorem Th132: :: MCART_2:130

for X1, X2, X3, X4, X5, X6, X7, X8 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} )

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} )

proof end;

theorem Th133: :: MCART_2:131

for X1, X2, X3, X4, X5, X6, X7, X8, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 )

proof end;

theorem :: MCART_2:132

for X1, X2, X3, X4, X5, X6, X7, X8, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} & [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 )

proof end;

theorem :: MCART_2:133

proof end;

theorem Th136: :: MCART_2:134

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 ex xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8]

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 ex xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8]

proof end;

definition

let X1, X2, X3, X4, X5, X6, X7, X8 be set ;

assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:];

func x `1 -> Element of X1 means :Def27: :: MCART_2:def 27

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x1;

existence

ex b_{1} being Element of X1 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x4;

existence

ex b_{1} being Element of X4 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x4

for b_{1}, b_{2} being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x4 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x5;

existence

ex b_{1} being Element of X5 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x5

for b_{1}, b_{2} being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x5 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x6;

existence

ex b_{1} being Element of X6 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x6

for b_{1}, b_{2} being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x6 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x7;

existence

ex b_{1} being Element of X7 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x7

for b_{1}, b_{2} being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x7 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x8;

existence

ex b_{1} being Element of X8 st

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x8

for b_{1}, b_{2} being Element of X8 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{1} = x8 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b_{2} = x8 ) holds

b_{1} = b_{2}

end;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:];

func x `1 -> Element of X1 means :Def27: :: MCART_2:def 27

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x1;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def28: :: MCART_2:def 28for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x2;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def29: :: MCART_2:def 29for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x3;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `4 -> Element of X4 means :Def30: :: MCART_2:def 30for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x4;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `5 -> Element of X5 means :Def31: :: MCART_2:def 31for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x5;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `6 -> Element of X6 means :Def32: :: MCART_2:def 32for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x6;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `7 -> Element of X7 means :Def33: :: MCART_2:def 33for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x7;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `8 -> Element of X8 means :Def34: :: MCART_2:def 34for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

it = x8;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def27 defines `1 MCART_2:def 27 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def28 defines `2 MCART_2:def 28 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def29 defines `3 MCART_2:def 29 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def30 defines `4 MCART_2:def 30 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def31 defines `5 MCART_2:def 31 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def32 defines `6 MCART_2:def 32 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def33 defines `7 MCART_2:def 33 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

:: deftheorem Def34 defines `8 MCART_2:def 34 :

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for b

( b

b

theorem :: MCART_2:135

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 ) by Def27, Def28, Def29, Def30, Def31, Def32, Def33, Def34;

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 ) by Def27, Def28, Def29, Def30, Def31, Def32, Def33, Def34;

theorem Th138: :: MCART_2:136

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7),(x `8)]

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7),(x `8)]

proof end;

theorem Th139: :: MCART_2:137

for X1, X2, X3, X4, X5, X6, X7, X8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds

( x `1 = ((((((x `1) `1) `1) `1) `1) `1) `1 & x `2 = ((((((x `1) `1) `1) `1) `1) `1) `2 & x `3 = (((((x `1) `1) `1) `1) `1) `2 & x `4 = ((((x `1) `1) `1) `1) `2 & x `5 = (((x `1) `1) `1) `2 & x `6 = ((x `1) `1) `2 & x `7 = (x `1) `2 & x `8 = x `2 )

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds

( x `1 = ((((((x `1) `1) `1) `1) `1) `1) `1 & x `2 = ((((((x `1) `1) `1) `1) `1) `1) `2 & x `3 = (((((x `1) `1) `1) `1) `1) `2 & x `4 = ((((x `1) `1) `1) `1) `2 & x `5 = (((x `1) `1) `1) `2 & x `6 = ((x `1) `1) `2 & x `7 = (x `1) `2 & x `8 = x `2 )

proof end;

theorem :: MCART_2:138

for X1, X2, X3, X4, X5, X6, X7, X8 being set st ( X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] or X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] or X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] or X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] or X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] or X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] or X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] or X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] ) holds

X1 = {}

X1 = {}

proof end;

theorem Th141: :: MCART_2:139

for X1, X2, X3, X4, X5, X6, X7, X8, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st [:X1,X2,X3,X4,X5,X6,X7,X8:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 & X8 meets Y8 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 & X8 meets Y8 )

proof end;

theorem Th142: :: MCART_2:140

for x1, x2, x3, x4, x5, x6, x7, x8 being set holds [:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8}:] = {[x1,x2,x3,x4,x5,x6,x7,x8]}

proof end;

theorem :: MCART_2:141

for X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 ) by Def27, Def28, Def29, Def30, Def31, Def32, Def33, Def34;

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} holds

for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 ) by Def27, Def28, Def29, Def30, Def31, Def32, Def33, Def34;

theorem :: MCART_2:142

for y1, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y1 = xx1 ) holds

y1 = x `1

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y1 = xx1 ) holds

y1 = x `1

proof end;

theorem :: MCART_2:143

for y2, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y2 = xx2 ) holds

y2 = x `2

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y2 = xx2 ) holds

y2 = x `2

proof end;

theorem :: MCART_2:144

for y3, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y3 = xx3 ) holds

y3 = x `3

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y3 = xx3 ) holds

y3 = x `3

proof end;

theorem :: MCART_2:145

for y4, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y4 = xx4 ) holds

y4 = x `4

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y4 = xx4 ) holds

y4 = x `4

proof end;

theorem :: MCART_2:146

for y5, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y5 = xx5 ) holds

y5 = x `5

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y5 = xx5 ) holds

y5 = x `5

proof end;

theorem :: MCART_2:147

for y6, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y6 = xx6 ) holds

y6 = x `6

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y6 = xx6 ) holds

y6 = x `6

proof end;

theorem :: MCART_2:148

for y7, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y7 = xx7 ) holds

y7 = x `7

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y7 = xx7 ) holds

y7 = x `7

proof end;

theorem :: MCART_2:149

for y8, X1, X2, X3, X4, X5, X6, X7, X8 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y8 = xx8 ) holds

y8 = x `8

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds

y8 = xx8 ) holds

y8 = x `8

proof end;

theorem Th152: :: MCART_2:150

for y, X1, X2, X3, X4, X5, X6, X7, X8 being set st y in [:X1,X2,X3,X4,X5,X6,X7,X8:] holds

ex x1, x2, x3, x4, x5, x6, x7, x8 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8] )

ex x1, x2, x3, x4, x5, x6, x7, x8 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8] )

proof end;

theorem Th153: :: MCART_2:151

for x1, x2, x3, x4, x5, x6, x7, x8, X1, X2, X3, X4, X5, X6, X7, X8 being set holds

( [x1,x2,x3,x4,x5,x6,x7,x8] in [:X1,X2,X3,X4,X5,X6,X7,X8:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 ) )

( [x1,x2,x3,x4,x5,x6,x7,x8] in [:X1,X2,X3,X4,X5,X6,X7,X8:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 ) )

proof end;

theorem :: MCART_2:152

for X1, X2, X3, X4, X5, X6, X7, X8, Z being set st ( for y being set holds

( y in Z iff ex x1, x2, x3, x4, x5, x6, x7, x8 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) ) holds

Z = [:X1,X2,X3,X4,X5,X6,X7,X8:]

( y in Z iff ex x1, x2, x3, x4, x5, x6, x7, x8 being set st

( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) ) holds

Z = [:X1,X2,X3,X4,X5,X6,X7,X8:]

proof end;

theorem Th155: :: MCART_2:153

for X1, X2, X3, X4, X5, X6, X7, X8, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} & Y5 <> {} & Y6 <> {} & Y7 <> {} & Y8 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]

for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] st x = y holds

( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 & x `5 = y `5 & x `6 = y `6 & x `7 = y `7 & x `8 = y `8 )

proof end;

theorem :: MCART_2:154

for X1, X2, X3, X4, X5, X6, X7, X8 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7

for A8 being Subset of X8

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 )

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7

for A8 being Subset of X8

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8:] holds

( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 & x `5 in A5 & x `6 in A6 & x `7 in A7 & x `8 in A8 )

proof end;

theorem Th157: :: MCART_2:155

for X1, X2, X3, X4, X5, X6, X7, X8, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7 & X8 c= Y8 holds

[:X1,X2,X3,X4,X5,X6,X7,X8:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]

[:X1,X2,X3,X4,X5,X6,X7,X8:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]

proof end;

theorem :: MCART_2:156

for X1, X2, X3, X4, X5, X6, X7, X8 being set

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7

for A8 being Subset of X8 holds [:A1,A2,A3,A4,A5,A6,A7,A8:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8:] by Th157;

for A1 being Subset of X1

for A2 being Subset of X2

for A3 being Subset of X3

for A4 being Subset of X4

for A5 being Subset of X5

for A6 being Subset of X6

for A7 being Subset of X7

for A8 being Subset of X8 holds [:A1,A2,A3,A4,A5,A6,A7,A8:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8:] by Th157;

begin

theorem :: MCART_2:157

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in Y holds

Y1 misses X ) )

proof end;

theorem :: MCART_2:158

for X being set st X <> {} holds

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE, YF being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in YF & YF in Y holds

Y1 misses X ) )

ex Y being set st

( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE, YF being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in YE & YE in YF & YF in Y holds

Y1 misses X ) )

proof end;

definition

let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ;

func [x1,x2,x3,x4,x5,x6,x7,x8,x9] -> set equals :: MCART_2:def 35

[[x1,x2,x3,x4,x5,x6,x7,x8],x9];

coherence

[[x1,x2,x3,x4,x5,x6,x7,x8],x9] is set ;

end;
func [x1,x2,x3,x4,x5,x6,x7,x8,x9] -> set equals :: MCART_2:def 35

[[x1,x2,x3,x4,x5,x6,x7,x8],x9];

coherence

[[x1,x2,x3,x4,x5,x6,x7,x8],x9] is set ;

:: deftheorem defines [ MCART_2:def 35 :

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7,x8],x9];

theorem Th161: :: MCART_2:159

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[[[[[[[x1,x2],x3],x4],x5],x6],x7],x8],x9]

proof end;

theorem :: MCART_2:160

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7],x8,x9] by MCART_1:def 3;

theorem :: MCART_2:161

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6],x7,x8,x9] by MCART_1:27;

theorem :: MCART_2:162

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5],x6,x7,x8,x9] by Th3;

theorem :: MCART_2:163

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4],x5,x6,x7,x8,x9] by Th41;

theorem :: MCART_2:164

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3],x4,x5,x6,x7,x8,x9]

proof end;

theorem :: MCART_2:165

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2],x3,x4,x5,x6,x7,x8,x9] by Th6;

theorem Th168: :: MCART_2:166

for x1, x2, x3, x4, x5, x6, x7, x8, x9, y1, y2, y3, y4, y5, y6, y7, y8, y9 being set st [x1,x2,x3,x4,x5,x6,x7,x8,x9] = [y1,y2,y3,y4,y5,y6,y7,y8,y9] holds

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 & x8 = y8 & x9 = y9 )

( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 & x8 = y8 & x9 = y9 )

proof end;

definition

let X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ;

func [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] -> set equals :: MCART_2:def 36

[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];

coherence

[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] is set ;

end;
func [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] -> set equals :: MCART_2:def 36

[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];

coherence

[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] is set ;

:: deftheorem defines [: MCART_2:def 36 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];

theorem Th169: :: MCART_2:167

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:]

proof end;

theorem :: MCART_2:168

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8,X9:] by ZFMISC_1:def 3;

theorem :: MCART_2:169

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6:],X7,X8,X9:] by MCART_1:49;

theorem :: MCART_2:170

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5:],X6,X7,X8,X9:] by Th9;

theorem :: MCART_2:171

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8,X9:] by Th47;

theorem :: MCART_2:172

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8,X9:]

proof end;

theorem :: MCART_2:173

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8,X9:] by Th12;

theorem Th176: :: MCART_2:174

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} )

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) iff [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} )

proof end;

theorem Th177: :: MCART_2:175

for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 & X9 = Y9 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 & X9 = Y9 )

proof end;

theorem :: MCART_2:176

for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} & [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 & X9 = Y9 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 & X5 = Y5 & X6 = Y6 & X7 = Y7 & X8 = Y8 & X9 = Y9 )

proof end;

theorem :: MCART_2:177

proof end;

theorem Th180: :: MCART_2:178

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 ex xx8 being Element of X8 ex xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9]

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 ex xx5 being Element of X5 ex xx6 being Element of X6 ex xx7 being Element of X7 ex xx8 being Element of X8 ex xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9]

proof end;

definition

let X1, X2, X3, X4, X5, X6, X7, X8, X9 be set ;

assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];

func x `1 -> Element of X1 means :Def37: :: MCART_2:def 37

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x1;

existence

ex b_{1} being Element of X1 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x4;

existence

ex b_{1} being Element of X4 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x4

for b_{1}, b_{2} being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x4 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x5;

existence

ex b_{1} being Element of X5 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x5

for b_{1}, b_{2} being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x5 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x6;

existence

ex b_{1} being Element of X6 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x6

for b_{1}, b_{2} being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x6 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x7;

existence

ex b_{1} being Element of X7 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x7

for b_{1}, b_{2} being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x7 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x8;

existence

ex b_{1} being Element of X8 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x8

for b_{1}, b_{2} being Element of X8 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x8 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x8 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x9;

existence

ex b_{1} being Element of X9 st

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x9

for b_{1}, b_{2} being Element of X9 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{1} = x9 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b_{2} = x9 ) holds

b_{1} = b_{2}

end;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} ) ;

let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];

func x `1 -> Element of X1 means :Def37: :: MCART_2:def 37

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x1;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def38: :: MCART_2:def 38for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x2;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def39: :: MCART_2:def 39for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x3;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `4 -> Element of X4 means :Def40: :: MCART_2:def 40for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x4;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `5 -> Element of X5 means :Def41: :: MCART_2:def 41for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x5;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `6 -> Element of X6 means :Def42: :: MCART_2:def 42for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x6;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `7 -> Element of X7 means :Def43: :: MCART_2:def 43for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x7;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `8 -> Element of X8 means :Def44: :: MCART_2:def 44for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x8;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `9 -> Element of X9 means :Def45: :: MCART_2:def 45for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

it = x9;

existence

ex b

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def37 defines `1 MCART_2:def 37 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def38 defines `2 MCART_2:def 38 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def39 defines `3 MCART_2:def 39 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def40 defines `4 MCART_2:def 40 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def41 defines `5 MCART_2:def 41 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def42 defines `6 MCART_2:def 42 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def43 defines `7 MCART_2:def 43 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def44 defines `8 MCART_2:def 44 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

:: deftheorem Def45 defines `9 MCART_2:def 45 :

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for b

( b

b

theorem :: MCART_2:179

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 & x `9 = x9 ) by Def37, Def38, Def39, Def40, Def41, Def42, Def43, Def44, Def45;

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 & x `9 = x9 ) by Def37, Def38, Def39, Def40, Def41, Def42, Def43, Def44, Def45;

theorem Th182: :: MCART_2:180

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7),(x `8),(x `9)]

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds x = [(x `1),(x `2),(x `3),(x `4),(x `5),(x `6),(x `7),(x `8),(x `9)]

proof end;

theorem Th183: :: MCART_2:181

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds

( x `1 = (((((((x `1) `1) `1) `1) `1) `1) `1) `1 & x `2 = (((((((x `1) `1) `1) `1) `1) `1) `1) `2 & x `3 = ((((((x `1) `1) `1) `1) `1) `1) `2 & x `4 = (((((x `1) `1) `1) `1) `1) `2 & x `5 = ((((x `1) `1) `1) `1) `2 & x `6 = (((x `1) `1) `1) `2 & x `7 = ((x `1) `1) `2 & x `8 = (x `1) `2 & x `9 = x `2 )

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds

( x `1 = (((((((x `1) `1) `1) `1) `1) `1) `1) `1 & x `2 = (((((((x `1) `1) `1) `1) `1) `1) `1) `2 & x `3 = ((((((x `1) `1) `1) `1) `1) `1) `2 & x `4 = (((((x `1) `1) `1) `1) `1) `2 & x `5 = ((((x `1) `1) `1) `1) `2 & x `6 = (((x `1) `1) `1) `2 & x `7 = ((x `1) `1) `2 & x `8 = (x `1) `2 & x `9 = x `2 )

proof end;

theorem :: MCART_2:182

for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 & X8 meets Y8 & X9 meets Y9 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 & X8 meets Y8 & X9 meets Y9 )

proof end;

theorem :: MCART_2:183

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds [:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8},{x9}:] = {[x1,x2,x3,x4,x5,x6,x7,x8,x9]}

proof end;

theorem :: MCART_2:184

for X1, X2, X3, X4, X5, X6, X7, X8, X9 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 & x `9 = x9 ) by Def37, Def38, Def39, Def40, Def41, Def42, Def43, Def44, Def45;

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} holds

for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds

( x `1 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 & x `5 = x5 & x `6 = x6 & x `7 = x7 & x `8 = x8 & x `9 = x9 ) by Def37, Def38, Def39, Def40, Def41, Def42, Def43, Def44, Def45;

theorem :: MCART_2:185

for y1, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8

for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds

y1 = xx1 ) holds

y1 = x `1

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8

for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds

y1 = xx1 ) holds

y1 = x `1

proof end;

theorem :: MCART_2:186

for y2, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8

for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds

y2 = xx2 ) holds

y2 = x `2

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8

for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds

y2 = xx2 ) holds

y2 = x `2

proof end;

theorem :: MCART_2:187

for y3, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8

for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds

y3 = xx3 ) holds

y3 = x

for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} & X9 <> {} & ( for xx1 being Element of X1

for xx2 being Element of X2

for xx3 being Element of X3

for xx4 being Element of X4

for xx5 being Element of X5

for xx6 being Element of X6

for xx7 being Element of X7

for xx8 being Element of X8

for xx9 being Element of X9 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds

y3 = xx3 ) holds

y3 = x