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

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

theorem :: MCART_2:10
canceled;

theorem :: MCART_2:11
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:12
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:13
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:14
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:15
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:16
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: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:] 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: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:]
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:19
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:20
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:21
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:22
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:23
for x1, x2, x3, x4, x5 being set holds [:{x1},{x2},{x3},{x4},{x5}:] = {[x1,x2,x3,x4,x5]}
proof end;

theorem :: MCART_2:24
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:25
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:26
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:27
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:28
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:29
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:30
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:31
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:32
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:33
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:34
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:35
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:36
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:37
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:38
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:39
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:40
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: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 MCART_1:def 3;

theorem :: MCART_2:43
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:44
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:45
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:46
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: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 ZFMISC_1:def 3;

theorem :: MCART_2:49
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:50
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:51
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:52
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:53
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:54
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: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:] 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: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:]
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:57
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:58
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:59
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:60
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:61
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:62
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:63
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:64
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:65
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:66
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:67
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:68
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:69
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:70
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:71
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:72
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: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
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:74
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:75
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:76
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:77
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: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]
proof end;

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] by MCART_1:def 3;

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 MCART_1:31;

theorem :: MCART_2:81
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:82
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:83
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:84
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: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:]
proof end;

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:] by ZFMISC_1:def 3;

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 MCART_1:53;

theorem :: MCART_2:88
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:89
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:90
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:91
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:92
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:93
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: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:] 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: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:]
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:96
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:97
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:98
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:99
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:100
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:101
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:102
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:103
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:104
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:105
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:106
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:107
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:108
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:109
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:110
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:111
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:112
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: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
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:114
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:115
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:116
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:117
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: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]
proof end;

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 MCART_1:def 3;

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] by MCART_1:31;

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

theorem :: MCART_2:122
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:123
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:124
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:125
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: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:]
proof end;

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 ZFMISC_1:def 3;

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:] by MCART_1:53;

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

theorem :: MCART_2:130
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:131
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:132
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:133
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:134
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:135
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: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:] 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: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:]
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:138
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:139
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:140
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:141
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:142
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:143
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:144
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:145
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:146
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:147
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:148
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:149
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:150
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:151
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:152
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:153
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:154
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:155
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: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
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:157
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:158
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:159
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:160
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: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]
proof end;

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 MCART_1:def 3;

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 MCART_1:31;

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] by Th3;

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

theorem :: MCART_2:166
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: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] by Th6;

theorem Th168: :: MCART_2:168
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: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:]
proof end;

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 ZFMISC_1:def 3;

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 MCART_1:53;

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:] by Th9;

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

theorem :: 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:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8,X9:]
proof end;

theorem :: MCART_2:175
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:176
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:177
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:178
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:179
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: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:] 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: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:]
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:182
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:183
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:184
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:185
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:186
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:187
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:188
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:189
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 `3
proof end;

theorem :: MCART_2:190
for y4, 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
y4 = xx4 ) holds
y4 = x `4
proof end;

theorem :: MCART_2:191
for y5, 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
y5 = xx5 ) holds
y5 = x `5
proof end;

theorem :: MCART_2:192
for y6, 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
y6 = xx6 ) holds
y6 = x `6
proof end;

theorem :: MCART_2:193
for y7, 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
y7 = xx7 ) holds
y7 = x `7
proof end;

theorem :: MCART_2:194
for y8, 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
y8 = xx8 ) holds
y8 = x `8
proof end;

theorem :: MCART_2:195
for y9, 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
y9 = xx9 ) holds
y9 = x `9
proof end;

theorem :: MCART_2:196
for y, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set st y in [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
ex x1, x2, x3, x4, x5, x6, x7, x8, x9 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 & x9 in X9 & y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] )
proof end;

theorem :: MCART_2:197
for x1, x2, x3, x4, x5, x6, x7, x8, x9, X1, X2, X3, X4, X5, X6, X7, X8, X9 being set holds
( [x1,x2,x3,x4,x5,x6,x7,x8,x9] in [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] 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 & x9 in X9 ) )
proof end;

theorem :: MCART_2:198
for X1, X2, X3, X4, X5, X6, X7, X8, X9, Z being set st ( for y being set holds
( y in Z iff ex x1, x2, x3, x4, x5, x6, x7, x8, x9 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 & x9 in X9 & y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] ) ) ) holds
Z = [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
proof end;

theorem Th199: :: MCART_2:199
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
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] 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 & x `9 = y `9 )
proof end;

theorem :: MCART_2:200
for X1, X2, X3, X4, X5, X6, X7, X8, X9 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 A9 being Subset of X9
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] 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 & x `9 in A9 )
proof end;

theorem Th201: :: MCART_2:201
for X1, X2, X3, X4, X5, X6, X7, X8, X9, Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 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 & X9 c= Y9 holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
proof end;

theorem :: MCART_2:202
for X1, X2, X3, X4, X5, X6, X7, X8, X9 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 A9 being Subset of X9 holds [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] by Th201;