:: N-Tuples and Cartesian Products for n=5
:: 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 ) )
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 ) )
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;

:: 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
for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5]
proof end;

theorem :: MCART_2:4
for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5]
proof end;

theorem Th6: :: MCART_2:5
for x1, x2, x3, x4, x5 being set holds [x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5]
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 )
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] ) ) )
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;

:: 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
for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:]
proof end;

theorem :: MCART_2:9
for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:]
proof end;

theorem Th12: :: MCART_2:10
for X1, X2, X3, X4, X5 being set holds [:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:]
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:] <> {} )
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 )
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 )
proof end;

theorem :: MCART_2:14
for X, Y being set st [:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:] holds
X = Y
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]
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 b1 being Element of X1 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x1
proof end;
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def4: :: MCART_2:def 4
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x2
proof end;
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def5: :: MCART_2:def 5
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x3
proof end;
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x3 ) holds
b1 = b2
proof end;
func x `4 -> Element of X4 means :Def6: :: MCART_2:def 6
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x4
proof end;
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x4 ) holds
b1 = b2
proof end;
func x `5 -> Element of X5 means :Def7: :: MCART_2:def 7
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x5
proof end;
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x5 ) holds
b1 = b2
proof end;
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 b7 being Element of X1 holds
( b7 = x `1 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b7 = x1 );

:: 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 b7 being Element of X2 holds
( b7 = x `2 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b7 = x2 );

:: 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 b7 being Element of X3 holds
( b7 = x `3 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b7 = x3 );

:: 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 b7 being Element of X4 holds
( b7 = x `4 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b7 = x4 );

:: 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 b7 being Element of X5 holds
( b7 = x `5 iff for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b7 = x5 );

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;

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)]
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 )
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 = {}
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 )
proof end;

theorem Th23: :: MCART_2:21
for x1, x2, x3, x4, x5 being set holds [:{x1},{x2},{x3},{x4},{x5}:] = {[x1,x2,x3,x4,x5]}
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;

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
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
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
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
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
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] )
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 ) )
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:]
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 )
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 )
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:]
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;

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;

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;

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;

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 ) )
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 ) )
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;

:: 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
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: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
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:42
for x1, x2, x3, x4, x5, x6 being set holds [x1,x2,x3,x4,x5,x6] = [[x1,x2],x3,x4,x5,x6] by Th6;

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 )
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] ) ) )
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;

:: 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
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: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:] <> {} )
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 )
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 )
proof end;

theorem :: MCART_2:52
for X, Y being set st [:X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y:] holds
X = Y
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]
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 b1 being Element of X1 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x1
proof end;
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def11: :: MCART_2:def 11
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x2
proof end;
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def12: :: MCART_2:def 12
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x3
proof end;
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x3 ) holds
b1 = b2
proof end;
func x `4 -> Element of X4 means :Def13: :: MCART_2:def 13
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x4
proof end;
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x4 ) holds
b1 = b2
proof end;
func x `5 -> Element of X5 means :Def14: :: MCART_2:def 14
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x5
proof end;
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x5 ) holds
b1 = b2
proof end;
func x `6 -> Element of X6 means :Def15: :: MCART_2:def 15
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
it = x6;
existence
ex b1 being Element of X6 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x6
proof end;
uniqueness
for b1, b2 being Element of X6 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x6 ) holds
b1 = b2
proof end;
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 b8 being Element of X1 holds
( b8 = x `1 iff for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b8 = x1 );

:: 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 b8 being Element of X2 holds
( b8 = x `2 iff for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b8 = x2 );

:: 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 b8 being Element of X3 holds
( b8 = x `3 iff for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b8 = x3 );

:: 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 b8 being Element of X4 holds
( b8 = x `4 iff for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b8 = x4 );

:: 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 b8 being Element of X5 holds
( b8 = x `5 iff for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b8 = x5 );

:: 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 b8 being Element of X6 holds
( b8 = x `6 iff for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b8 = x6 );

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;

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)]
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 )
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 = {}
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 )
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;

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
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
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
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
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
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
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] )
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 ) )
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:]
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 )
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 )
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:]
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;

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 ) )
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 ) )
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;

:: 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
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: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 )
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] ) ) )
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;

:: 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:] <> {} )
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 )
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 )
proof end;

theorem :: MCART_2:91
for X, Y being set st [:X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
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]
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 b1 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
b1 = x1
proof end;
uniqueness
for b1, b2 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
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def19: :: MCART_2:def 19
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x2;
existence
ex b1 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
b1 = x2
proof end;
uniqueness
for b1, b2 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
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def20: :: MCART_2:def 20
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x3;
existence
ex b1 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
b1 = x3
proof end;
uniqueness
for b1, b2 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
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x3 ) holds
b1 = b2
proof end;
func x `4 -> Element of X4 means :Def21: :: MCART_2:def 21
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x4;
existence
ex b1 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
b1 = x4
proof end;
uniqueness
for b1, b2 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
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x4 ) holds
b1 = b2
proof end;
func x `5 -> Element of X5 means :Def22: :: MCART_2:def 22
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x5;
existence
ex b1 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
b1 = x5
proof end;
uniqueness
for b1, b2 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
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x5 ) holds
b1 = b2
proof end;
func x `6 -> Element of X6 means :Def23: :: MCART_2:def 23
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x6;
existence
ex b1 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
b1 = x6
proof end;
uniqueness
for b1, b2 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
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x6 ) holds
b1 = b2
proof end;
func x `7 -> Element of X7 means :Def24: :: MCART_2:def 24
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x7;
existence
ex b1 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
b1 = x7
proof end;
uniqueness
for b1, b2 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
b1 = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x7 ) holds
b1 = b2
proof end;
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 b9 being Element of X1 holds
( b9 = x `1 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x1 );

:: 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 b9 being Element of X2 holds
( b9 = x `2 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x2 );

:: 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 b9 being Element of X3 holds
( b9 = x `3 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x3 );

:: 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 b9 being Element of X4 holds
( b9 = x `4 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x4 );

:: 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 b9 being Element of X5 holds
( b9 = x `5 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x5 );

:: 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 b9 being Element of X6 holds
( b9 = x `6 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x6 );

:: 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 b9 being Element of X7 holds
( b9 = x `7 iff for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x7 );

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;

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)]
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 )
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 = {}
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 )
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;

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
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
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
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
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
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
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
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] )
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 ) )
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:]
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 )
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 )
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:]
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;

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 ) )
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 ) )
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;

:: 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 )
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] ) ) )
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;

:: 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:] <> {} )
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 )
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 )
proof end;

theorem :: MCART_2:133
for X, Y being set st [:X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
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]
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 b1 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
b1 = x1
proof end;
uniqueness
for b1, b2 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
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def28: :: MCART_2:def 28
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 b1 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
b1 = x2
proof end;
uniqueness
for b1, b2 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
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def29: :: MCART_2:def 29
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 b1 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
b1 = x3
proof end;
uniqueness
for b1, b2 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
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x3 ) holds
b1 = b2
proof end;
func x `4 -> Element of X4 means :Def30: :: MCART_2:def 30
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 b1 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
b1 = x4
proof end;
uniqueness
for b1, b2 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
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x4 ) holds
b1 = b2
proof end;
func x `5 -> Element of X5 means :Def31: :: MCART_2:def 31
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 b1 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
b1 = x5
proof end;
uniqueness
for b1, b2 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
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x5 ) holds
b1 = b2
proof end;
func x `6 -> Element of X6 means :Def32: :: MCART_2:def 32
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 b1 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
b1 = x6
proof end;
uniqueness
for b1, b2 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
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x6 ) holds
b1 = b2
proof end;
func x `7 -> Element of X7 means :Def33: :: MCART_2:def 33
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 b1 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
b1 = x7
proof end;
uniqueness
for b1, b2 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
b1 = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x7 ) holds
b1 = b2
proof end;
func x `8 -> Element of X8 means :Def34: :: MCART_2:def 34
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 b1 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
b1 = x8
proof end;
uniqueness
for b1, b2 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
b1 = x8 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x8 ) holds
b1 = b2
proof end;
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 b10 being Element of X1 holds
( b10 = x `1 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x1 );

:: 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 b10 being Element of X2 holds
( b10 = x `2 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x2 );

:: 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 b10 being Element of X3 holds
( b10 = x `3 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x3 );

:: 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 b10 being Element of X4 holds
( b10 = x `4 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x4 );

:: 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 b10 being Element of X5 holds
( b10 = x `5 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x5 );

:: 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 b10 being Element of X6 holds
( b10 = x `6 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x6 );

:: 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 b10 being Element of X7 holds
( b10 = x `7 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x7 );

:: 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 b10 being Element of X8 holds
( b10 = x `8 iff for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x8 );

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;

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)]
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 )
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 = {}
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 )
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;

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
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
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
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
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
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
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
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
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] )
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 ) )
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:]
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 )
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 )
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:]
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;

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 ) )
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 ) )
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;

:: 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 )
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;

:: 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:] <> {} )
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 )
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 )
proof end;

theorem :: MCART_2:177
for X, Y being set st [:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
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]
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 b1 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
b1 = x1
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def38: :: MCART_2:def 38
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 b1 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
b1 = x2
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def39: :: MCART_2:def 39
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 b1 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
b1 = x3
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x3 ) holds
b1 = b2
proof end;
func x `4 -> Element of X4 means :Def40: :: MCART_2:def 40
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 b1 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
b1 = x4
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x4 ) holds
b1 = b2
proof end;
func x `5 -> Element of X5 means :Def41: :: MCART_2:def 41
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 b1 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
b1 = x5
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x5 ) holds
b1 = b2
proof end;
func x `6 -> Element of X6 means :Def42: :: MCART_2:def 42
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 b1 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
b1 = x6
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x6 ) holds
b1 = b2
proof end;
func x `7 -> Element of X7 means :Def43: :: MCART_2:def 43
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 b1 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
b1 = x7
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x7 ) holds
b1 = b2
proof end;
func x `8 -> Element of X8 means :Def44: :: MCART_2:def 44
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 b1 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
b1 = x8
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x8 ) holds
b1 = b2
proof end;
func x `9 -> Element of X9 means :Def45: :: MCART_2:def 45
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 b1 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
b1 = x9
proof end;
uniqueness
for b1, b2 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
b1 = 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
b2 = x9 ) holds
b1 = b2
proof end;
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 b11 being Element of X1 holds
( b11 = x `1 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x1 );

:: 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 b11 being Element of X2 holds
( b11 = x `2 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x2 );

:: 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 b11 being Element of X3 holds
( b11 = x `3 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x3 );

:: 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 b11 being Element of X4 holds
( b11 = x `4 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x4 );

:: 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 b11 being Element of X5 holds
( b11 = x `5 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x5 );

:: 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 b11 being Element of X6 holds
( b11 = x `6 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x6 );

:: 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 b11 being Element of X7 holds
( b11 = x `7 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x7 );

:: 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 b11 being Element of X8 holds
( b11 = x `8 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x8 );

:: 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 b11 being Element of X9 holds
( b11 = x `9 iff for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x9 );

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;

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)]
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 )
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 )
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;

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
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
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