:: Tuples and Cartesian Products for n=6
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 15, 1990
:: Copyright (c) 1990 Association of Mizar Users


theorem :: MCART_3:1
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 Th2: :: MCART_3:2
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_3:def 1
[[x1,x2,x3,x4,x5],x6];
correctness
coherence
[[x1,x2,x3,x4,x5],x6] is set ;
;
end;

:: deftheorem defines [ MCART_3:def 1 :
for x1, x2, x3, x4, x5, x6 being set holds [x1,x2,x3,x4,x5,x6] = [[x1,x2,x3,x4,x5],x6];

theorem MC33: :: MCART_3:3
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_3:4
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_3:5
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 Th6: :: MCART_3:6
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 Th7: :: MCART_3:7
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 Th8: :: MCART_3:8
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_3:def 2
[:[:X1,X2,X3,X4,X5:],X6:];
coherence
[:[:X1,X2,X3,X4,X5:],X6:] is set ;
end;

:: deftheorem defines [: MCART_3:def 2 :
for X1, X2, X3, X4, X5, X6 being set holds [:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3,X4,X5:],X6:];

theorem MC39: :: MCART_3:9
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_3:10
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_3:11
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 Th12: :: MCART_3:12
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 Th13: :: MCART_3:13
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 Th14: :: MCART_3:14
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_3:15
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_3:16
for X, Y being set st [:X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y:] holds
X = Y
proof end;

theorem Th17: :: MCART_3:17
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 :Def3: :: MCART_3:def 3
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 :Def4: :: MCART_3:def 4
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 :Def5: :: MCART_3:def 5
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 :Def6: :: MCART_3:def 6
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 :Def7: :: MCART_3:def 7
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 :Def8: :: MCART_3:def 8
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 Def3 defines `1 MCART_3:def 3 :
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 Def4 defines `2 MCART_3:def 4 :
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 Def5 defines `3 MCART_3:def 5 :
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 Def6 defines `4 MCART_3:def 6 :
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 Def7 defines `5 MCART_3:def 7 :
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 Def8 defines `6 MCART_3:def 8 :
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_3:18
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 Def3, Def4, Def5, Def6, Def7, Def8;

theorem Th19: :: MCART_3:19
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 Th20: :: MCART_3:20
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 Th21: :: MCART_3:21
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_3:22
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 Th23: :: MCART_3:23
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_3:24
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 Def3, Def4, Def5, Def6, Def7, Def8;

theorem :: MCART_3:25
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_3:26
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_3:27
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_3:28
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_3:29
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_3:30
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 Th31: :: MCART_3:31
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 Th32: :: MCART_3:32
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_3:33
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 Th34: :: MCART_3:34
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_3:35
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 Th36: :: MCART_3:36
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_3:37
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 Th36;

theorem :: MCART_3:38
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, 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 Th39: :: MCART_3: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, 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_3:def 9
[[x1,x2,x3,x4,x5,x6],x7];
correctness
coherence
[[x1,x2,x3,x4,x5,x6],x7] is set ;
;
end;

:: deftheorem defines [ MCART_3:def 9 :
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 MC340: :: MCART_3:40
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_3:41
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_3:42
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_3:43
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 MC344: :: MCART_3:44
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 MC345: :: MCART_3:45
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 Th46: :: MCART_3:46
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_3:def 10
[:[:X1,X2,X3,X4,X5,X6:],X7:];
correctness
coherence
[:[:X1,X2,X3,X4,X5,X6:],X7:] is set ;
;
end;

:: deftheorem defines [: MCART_3:def 10 :
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 MC347: :: MCART_3:47
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_3:48
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_3:49
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_3:50
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 MC351: :: MCART_3:51
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 MC352: :: MCART_3:52
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 MC353: :: MCART_3:53
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_3:54
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_3:55
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 MC356: :: MCART_3:56
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 :Def11: :: MCART_3:def 11
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 :Def12: :: MCART_3:def 12
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 :Def13: :: MCART_3:def 13
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 :Def14: :: MCART_3:def 14
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 :Def15: :: MCART_3:def 15
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 :Def16: :: MCART_3:def 16
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 :Def17: :: MCART_3:def 17
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 Def11 defines `1 MCART_3:def 11 :
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 Def12 defines `2 MCART_3:def 12 :
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 Def13 defines `3 MCART_3:def 13 :
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 Def14 defines `4 MCART_3:def 14 :
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 Def15 defines `5 MCART_3:def 15 :
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 Def16 defines `6 MCART_3:def 16 :
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 Def17 defines `7 MCART_3:def 17 :
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_3:57
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 Def11, Def12, Def13, Def14, Def15, Def16, Def17;

theorem Th58: :: MCART_3:58
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 Th59: :: MCART_3:59
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 MC360: :: MCART_3:60
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 MC361: :: MCART_3:61
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 MC362: :: MCART_3:62
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_3:63
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 Def11, Def12, Def13, Def14, Def15, Def16, Def17;

theorem :: MCART_3:64
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_3:65
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_3:66
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_3:67
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_3:68
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_3:69
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_3:70
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 MC371: :: MCART_3:71
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 MC372: :: MCART_3:72
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_3:73
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 Th74: :: MCART_3:74
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_3:75
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 MC376: :: MCART_3:76
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_3:77
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 MC376;

theorem :: MCART_3:78
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 Th2: :: MCART_3:79
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_3:def 18
[[x1,x2,x3,x4,x5,x6,x7],x8];
correctness
coherence
[[x1,x2,x3,x4,x5,x6,x7],x8] is set ;
;
end;

:: deftheorem defines [ MCART_3:def 18 :
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 Th3: :: MCART_3:80
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_3:81
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_3:82
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_3:83
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_3:84
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_3:85
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 MC344;

theorem Th9: :: MCART_3:86
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 Th10: :: MCART_3:87
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_3:def 19
[:[:X1,X2,X3,X4,X5,X6,X7:],X8:];
correctness
coherence
[:[:X1,X2,X3,X4,X5,X6,X7:],X8:] is set ;
;
end;

:: deftheorem defines [: MCART_3:def 19 :
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 Th11: :: MCART_3:88
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_3:89
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_3:90
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_3:91
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_3:92
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_3:93
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 MC351;

theorem Th17: :: MCART_3:94
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 Th18: :: MCART_3:95
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_3:96
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_3:97
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 Th21: :: MCART_3:98
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 :Def3: :: MCART_3:def 20
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 :Def4: :: MCART_3:def 21
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 :Def5: :: MCART_3:def 22
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 :Def6: :: MCART_3:def 23
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 :Def7: :: MCART_3:def 24
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 :Def8: :: MCART_3:def 25
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 :Def9: :: MCART_3:def 26
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 :Def10: :: MCART_3: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 = 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 Def3 defines `1 MCART_3:def 20 :
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 Def4 defines `2 MCART_3:def 21 :
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 Def5 defines `3 MCART_3:def 22 :
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 Def6 defines `4 MCART_3:def 23 :
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 Def7 defines `5 MCART_3:def 24 :
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 Def8 defines `6 MCART_3:def 25 :
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 Def9 defines `7 MCART_3:def 26 :
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 Def10 defines `8 MCART_3: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 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_3:99
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 Def3, Def4, Def5, Def6, Def7, Def8, Def9, Def10;

theorem Th23: :: MCART_3:100
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 Th24: :: MCART_3:101
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_3:102
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 Th26: :: MCART_3:103
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 Th27: :: MCART_3:104
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_3:105
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 Def3, Def4, Def5, Def6, Def7, Def8, Def9, Def10;

theorem :: MCART_3:106
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_3:107
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_3:108
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_3:109
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_3:110
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_3:111
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_3:112
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_3:113
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 Th37: :: MCART_3:114
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 Th38: :: MCART_3:115
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_3:116
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 Th40: :: MCART_3:117
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_3:118
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 Th42: :: MCART_3:119
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_3:120
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 Th42;

theorem :: MCART_3:121
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_3:122
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_3:def 28
[[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_3:def 28 :
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 Th46: :: MCART_3:123
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_3:124
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_3:125
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_3:126
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_2:3;

theorem :: MCART_3:127
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_3:128
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_3:129
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 MC344;

theorem Th53: :: MCART_3:130
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_3:def 29
[:[: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_3:def 29 :
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 Th54: :: MCART_3:131
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_3:132
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_3:133
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_3:134
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_2:9;

theorem :: MCART_3:135
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_3:136
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_3:137
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 MC351;

theorem Th61: :: MCART_3:138
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 Th62: :: MCART_3:139
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_3:140
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_3:141
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 Th65: :: MCART_3:142
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 :Def13: :: MCART_3:def 30
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 :Def14: :: MCART_3:def 31
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 :Def15: :: MCART_3:def 32
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 :Def16: :: MCART_3:def 33
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 :Def17: :: MCART_3:def 34
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 :Def18: :: MCART_3:def 35
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 :Def19: :: MCART_3:def 36
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 :Def20: :: MCART_3: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 = 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 :Def21: :: MCART_3: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 = 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 Def13 defines `1 MCART_3:def 30 :
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 Def14 defines `2 MCART_3:def 31 :
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 Def15 defines `3 MCART_3:def 32 :
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 Def16 defines `4 MCART_3:def 33 :
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 Def17 defines `5 MCART_3:def 34 :
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 Def18 defines `6 MCART_3:def 35 :
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 Def19 defines `7 MCART_3:def 36 :
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 Def20 defines `8 MCART_3: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 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 Def21 defines `9 MCART_3: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 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_3:143
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 Def13, Def14, Def15, Def16, Def17, Def18, Def19, Def20, Def21;

theorem Th67: :: MCART_3:144
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 Th68: :: MCART_3:145
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_3:146
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_3:147
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_3:148
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 Def13, Def14, Def15, Def16, Def17, Def18, Def19, Def20, Def21;

theorem :: MCART_3:149
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_3:150
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_3:151
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_3:152
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_3:153
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_3:154
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_3:155
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_3:156
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_3:157
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_3:158
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_3:159
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_3:160
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 Th84: :: MCART_3:161
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_3:162
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 Th86: :: MCART_3:163
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_3:164
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 Th86;