:: MCART_1 semantic presentation

begin


theorem :: MCART_1:1
canceled;

theorem :: MCART_1:2
canceled;

theorem :: MCART_1:3
canceled;

theorem :: MCART_1:4
canceled;

theorem :: MCART_1:5
canceled;

theorem :: MCART_1:6
canceled;

theorem Th7: :: MCART_1:7
for x, y being set holds
( [x,y] `1 = x & [x,y] `2 = y ) ;

theorem Th8: :: MCART_1:8
for p being pair set holds [(p `1),(p `2)] = p ;

theorem :: MCART_1:9
for X being set st X <> {} holds
ex v being set st
( v in X & ( for x, y being set holds
( ( not x in X & not y in X ) or not v = [x,y] ) ) )
proof
let X be set ; ::_thesis: ( X <> {} implies ex v being set st
( v in X & ( for x, y being set holds
( ( not x in X & not y in X ) or not v = [x,y] ) ) ) )
assume  X <> {} ; ::_thesis: ex v being set st
( v in X & ( for x, y being set holds
( ( not x in X & not y in X ) or not v = [x,y] ) ) )
then consider Y being set  such that
A1: Y in X and
A2: for Y1 being set holds
( not Y1 in Y or Y1 misses X ) by XREGULAR:2;
take v = Y; ::_thesis: ( v in X & ( for x, y being set holds
( ( not x in X & not y in X ) or not v = [x,y] ) ) )
thus  v in X by A1; ::_thesis: for x, y being set holds
( ( not x in X & not y in X ) or not v = [x,y] )
given x, y being set  such that A3: ( x in X or y in X ) and
A4: v = [x,y] ; ::_thesis: contradiction
A5: {x,y} in Y by A4, TARSKI:def_2;
 ( x in {x,y} & y in {x,y} ) by TARSKI:def_2;
hence  contradiction by A2, A5, A3, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th10: :: MCART_1:10
for z, X, Y being set st z in [:X,Y:] holds
( z `1 in X & z `2 in Y )
proof
let z, X, Y be set ; ::_thesis: ( z in [:X,Y:] implies ( z `1 in X & z `2 in Y ) )
assume  z in [:X,Y:] ; ::_thesis: ( z `1 in X & z `2 in Y )
then consider x, y being set  such that
W: ( x in X & y in Y & z = [x,y] ) by ZFMISC_1:def_2;
 ( [x,y] `1 = x & [x,y] `2 = y ) ;
hence  ( z `1 in X & z `2 in Y ) by W; ::_thesis: verum
end;

theorem :: MCART_1:11
for z, X, Y being set st ex x, y being set st z = [x,y] & z `1 in X & z `2 in Y holds
z in [:X,Y:]
proof
let z, X, Y be set ; ::_thesis: ( ex x, y being set st z = [x,y] & z `1 in X & z `2 in Y implies z in [:X,Y:] )
assume  ex x, y being set st z = [x,y] ; ::_thesis: ( not z `1 in X or not z `2 in Y or z in [:X,Y:] )
then  [(z `1),(z `2)] = z by Th8;
hence  ( not z `1 in X or not z `2 in Y or z in [:X,Y:] ) by ZFMISC_1:def_2; ::_thesis: verum
end;

theorem :: MCART_1:12
for z, x, Y being set st z in [:{x},Y:] holds
( z `1 = x & z `2 in Y )
proof
let z, x, Y be set ; ::_thesis: ( z in [:{x},Y:] implies ( z `1 = x & z `2 in Y ) )
assume A1: z in [:{x},Y:] ; ::_thesis: ( z `1 = x & z `2 in Y )
then  z `1 in {x} by Th10;
hence  ( z `1 = x & z `2 in Y ) by A1, Th10, TARSKI:def_1; ::_thesis: verum
end;

theorem :: MCART_1:13
for z, X, y being set st z in [:X,{y}:] holds
( z `1 in X & z `2 = y )
proof
let z, X, y be set ; ::_thesis: ( z in [:X,{y}:] implies ( z `1 in X & z `2 = y ) )
assume A1: z in [:X,{y}:] ; ::_thesis: ( z `1 in X & z `2 = y )
then  z `2 in {y} by Th10;
hence  ( z `1 in X & z `2 = y ) by A1, Th10, TARSKI:def_1; ::_thesis: verum
end;

theorem :: MCART_1:14
for z, x, y being set st z in [:{x},{y}:] holds
( z `1 = x & z `2 = y )
proof
let z, x, y be set ; ::_thesis: ( z in [:{x},{y}:] implies ( z `1 = x & z `2 = y ) )
assume  z in [:{x},{y}:] ; ::_thesis: ( z `1 = x & z `2 = y )
then  ( z `1 in {x} & z `2 in {y} ) by Th10;
hence  ( z `1 = x & z `2 = y ) by TARSKI:def_1; ::_thesis: verum
end;

theorem :: MCART_1:15
for z, x1, x2, Y being set st z in [:{x1,x2},Y:] holds
( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y )
proof
let z, x1, x2, Y be set ; ::_thesis: ( z in [:{x1,x2},Y:] implies ( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y ) )
assume A1: z in [:{x1,x2},Y:] ; ::_thesis: ( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y )
then  z `1 in {x1,x2} by Th10;
hence  ( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y ) by A1, Th10, TARSKI:def_2; ::_thesis: verum
end;

theorem :: MCART_1:16
for z, X, y1, y2 being set st z in [:X,{y1,y2}:] holds
( z `1 in X & ( z `2 = y1 or z `2 = y2 ) )
proof
let z, X, y1, y2 be set ; ::_thesis: ( z in [:X,{y1,y2}:] implies ( z `1 in X & ( z `2 = y1 or z `2 = y2 ) ) )
assume A1: z in [:X,{y1,y2}:] ; ::_thesis: ( z `1 in X & ( z `2 = y1 or z `2 = y2 ) )
then  z `2 in {y1,y2} by Th10;
hence  ( z `1 in X & ( z `2 = y1 or z `2 = y2 ) ) by A1, Th10, TARSKI:def_2; ::_thesis: verum
end;

theorem :: MCART_1:17
for z, x1, x2, y being set st z in [:{x1,x2},{y}:] holds
( ( z `1 = x1 or z `1 = x2 ) & z `2 = y )
proof
let z, x1, x2, y be set ; ::_thesis: ( z in [:{x1,x2},{y}:] implies ( ( z `1 = x1 or z `1 = x2 ) & z `2 = y ) )
assume  z in [:{x1,x2},{y}:] ; ::_thesis: ( ( z `1 = x1 or z `1 = x2 ) & z `2 = y )
then  ( z `1 in {x1,x2} & z `2 in {y} ) by Th10;
hence  ( ( z `1 = x1 or z `1 = x2 ) & z `2 = y ) by TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;

theorem :: MCART_1:18
for z, x, y1, y2 being set st z in [:{x},{y1,y2}:] holds
( z `1 = x & ( z `2 = y1 or z `2 = y2 ) )
proof
let z, x, y1, y2 be set ; ::_thesis: ( z in [:{x},{y1,y2}:] implies ( z `1 = x & ( z `2 = y1 or z `2 = y2 ) ) )
assume  z in [:{x},{y1,y2}:] ; ::_thesis: ( z `1 = x & ( z `2 = y1 or z `2 = y2 ) )
then  ( z `1 in {x} & z `2 in {y1,y2} ) by Th10;
hence  ( z `1 = x & ( z `2 = y1 or z `2 = y2 ) ) by TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;

theorem :: MCART_1:19
for z, x1, x2, y1, y2 being set st z in [:{x1,x2},{y1,y2}:] holds
( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) )
proof
let z, x1, x2, y1, y2 be set ; ::_thesis: ( z in [:{x1,x2},{y1,y2}:] implies ( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) ) )
assume  z in [:{x1,x2},{y1,y2}:] ; ::_thesis: ( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) )
then  ( z `1 in {x1,x2} & z `2 in {y1,y2} ) by Th10;
hence  ( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th20: :: MCART_1:20
for x being set st ex y, z being set st x = [y,z] holds
( x <> x `1 & x <> x `2 )
proof
let x be set ; ::_thesis: ( ex y, z being set st x = [y,z] implies ( x <> x `1 & x <> x `2 ) )
given y, z being set  such that A1: x = [y,z] ; ::_thesis: ( x <> x `1 & x <> x `2 )
X: ( [y,z] `1 = y & [y,z] `2 = z ) ;
now__::_thesis:_not_y_=_x
assume  y = x ; ::_thesis: contradiction
then  {{y,z},{y}} in {y} by A1, TARSKI:def_1;
hence  contradiction by TARSKI:def_2; ::_thesis: verum
end;
hence  x <> x `1 by A1, X; ::_thesis: x <> x `2
now__::_thesis:_not_z_=_x
assume  z = x ; ::_thesis: contradiction
then  {{y,z},{y}} in {y,z} by A1, TARSKI:def_2;
hence  contradiction by TARSKI:def_2; ::_thesis: verum
end;
hence  x <> x `2 by A1, X; ::_thesis: verum
end;

theorem Th21: :: MCART_1:21
for x being set
for R being Relation st x in R holds
x = [(x `1),(x `2)]
proof
let x be set ; ::_thesis: for R being Relation st x in R holds
x = [(x `1),(x `2)]
let R be Relation; ::_thesis: ( x in R implies x = [(x `1),(x `2)] )
assume  x in R ; ::_thesis: x = [(x `1),(x `2)]
then  ex x1, x2 being set st x = [x1,x2] by RELAT_1:def_1;
hence  x = [(x `1),(x `2)] by Th8; ::_thesis: verum
end;

theorem :: MCART_1:22
for X, Y being set st X <> {} & Y <> {} holds
for x being Element of [:X,Y:] holds x = [(x `1),(x `2)] by Th21;

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
let X1, X2 be set ; ::_thesis: ( X1 <> {} & X2 <> {} implies for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2] )
assume A1: ( X1 <> {} & X2 <> {} ) ; ::_thesis: for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]
let x be Element of [:X1,X2:]; ::_thesis: ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]
reconsider xx2 = x `2 as Element of X2 by A1, Th10;
reconsider xx1 = x `1 as Element of X1 by A1, Th10;
take  xx1 ; ::_thesis: ex xx2 being Element of X2 st x = [xx1,xx2]
take  xx2 ; ::_thesis: x = [xx1,xx2]
thus  x = [xx1,xx2] by A1, Th21; ::_thesis: verum
end;

theorem Th23: :: MCART_1:23
for x1, x2, y1, y2 being set holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof
let x1, x2, y1, y2 be set ; ::_thesis: [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
thus [:{x1,x2},{y1,y2}:] = [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by ZFMISC_1:109
.= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by ZFMISC_1:30
.= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by ZFMISC_1:30
.= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5 ; ::_thesis: verum
end;

theorem Th24: :: MCART_1:24
for X, Y being set st X <> {} & Y <> {} holds
for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
proof
let X, Y be set ; ::_thesis: ( X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 ) )
assume A1: ( X <> {} & Y <> {} ) ; ::_thesis: for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
let x be Element of [:X,Y:]; ::_thesis: ( x <> x `1 & x <> x `2 )
 x = [(x `1),(x `2)] by A1, Th21;
hence  ( x <> x `1 & x <> x `2 ) by Th20; ::_thesis: verum
end;

theorem :: MCART_1:25
canceled;

theorem Th26: :: MCART_1:26
for X being set st X <> {} holds
ex v being set st
( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )
proof
let X be set ; ::_thesis: ( X <> {} implies ex v being set st
( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) ) )
assume  X <> {} ; ::_thesis: ex v being set st
( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )
then consider Y being set  such that
A1: Y in X and
A2: for Y1, Y2, Y3 being set holds
( not Y1 in Y2 or not Y2 in Y3 or not Y3 in Y or Y1 misses X ) by XREGULAR:4;
take v = Y; ::_thesis: ( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )
thus  v in X by A1; ::_thesis: for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] )
given x, y, z being set  such that A3: ( x in X or y in X ) and
A4: v = [x,y,z] ; ::_thesis: contradiction
set Y1 = {x,y};
set Y2 = {{x,y},{x}};
set Y3 = {{{x,y},{x}},z};
B5: ( x in {x,y} & y in {x,y} ) by TARSKI:def_2;
A6: {{{x,y},{x}},z} in Y by A4, TARSKI:def_2;
 ( {x,y} in {{x,y},{x}} & {{x,y},{x}} in {{{x,y},{x}},z} ) by TARSKI:def_2;
hence  contradiction by A2, B5, A6, A3, XBOOLE_0:3; ::_thesis: verum
end;

theorem :: MCART_1:27
canceled;

theorem :: MCART_1:28
canceled;

theorem :: MCART_1:29
canceled;

theorem Th30: :: MCART_1:30
for X being set st X <> {} holds
ex v being set st
( v in X & ( for x1, x2, x3, x4 being set holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
proof
let X be set ; ::_thesis: ( X <> {} implies ex v being set st
( v in X & ( for x1, x2, x3, x4 being set holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) ) )
assume  X <> {} ; ::_thesis: ex v being set st
( v in X & ( for x1, x2, x3, x4 being set holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
then consider Y being set  such that
A1: Y in X and
A2: for Y1, Y2, Y3, Y4, Y5 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds
Y1 misses X by XREGULAR:6;
take v = Y; ::_thesis: ( v in X & ( for x1, x2, x3, x4 being set holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
thus  v in X by A1; ::_thesis: for x1, x2, x3, x4 being set holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] )
given x1, x2, x3, x4 being set  such that A3: ( x1 in X or x2 in X ) and
A4: v = [x1,x2,x3,x4] ; ::_thesis: contradiction
set Y1 = {x1,x2};
set Y2 = {{x1,x2},{x1}};
set Y3 = {{{x1,x2},{x1}},x3};
set Y4 = {{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}};
set Y5 = {{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4};
A5: ( {{{x1,x2},{x1}},x3} in {{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}} & {{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}} in {{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4} ) by TARSKI:def_2;
A6: {{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4} in Y by A4, TARSKI:def_2;
B7: ( x1 in {x1,x2} & x2 in {x1,x2} ) by TARSKI:def_2;
 ( {x1,x2} in {{x1,x2},{x1}} & {{x1,x2},{x1}} in {{{x1,x2},{x1}},x3} ) by TARSKI:def_2;
hence  contradiction by A2, B7, A5, A6, A3, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th31: :: MCART_1:31
for X1, X2, X3 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} )
proof
let X1, X2, X3 be set ; ::_thesis: ( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} )
A1: ( ( X1 <> {} & X2 <> {} ) iff [:X1,X2:] <> {} ) by ZFMISC_1:90;
 [:[:X1,X2:],X3:] = [:X1,X2,X3:] by ZFMISC_1:def_3;
hence  ( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} ) by A1, ZFMISC_1:90; ::_thesis: verum
end;


theorem Th32: :: MCART_1:32
for X1, X2, X3, Y1, Y2, Y3 being set st X1 <> {} & X2 <> {} & X3 <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 )
proof
let X1, X2, X3, Y1, Y2, Y3 be set ; ::_thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) )
A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def_3;
assume A2: ( X1 <> {} & X2 <> {} ) ; ::_thesis: ( not X3 <> {} or not [:X1,X2,X3:] = [:Y1,Y2,Y3:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) )
assume A4: X3 <> {} ; ::_thesis: ( not [:X1,X2,X3:] = [:Y1,Y2,Y3:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) )
assume  [:X1,X2,X3:] = [:Y1,Y2,Y3:] ; ::_thesis: ( X1 = Y1 & X2 = Y2 & X3 = Y3 )
then A5: [:[:X1,X2:],X3:] = [:[:Y1,Y2:],Y3:] by A1, ZFMISC_1:def_3;
then  [:X1,X2:] = [:Y1,Y2:] by A2, A4, ZFMISC_1:110;
hence  ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) by A2, A4, A5, ZFMISC_1:110; ::_thesis: verum
end;

theorem :: MCART_1:33
for X1, X2, X3, Y1, Y2, Y3 being set st [:X1,X2,X3:] <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 )
proof
let X1, X2, X3, Y1, Y2, Y3 be set ; ::_thesis: ( [:X1,X2,X3:] <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) )
assume A1: [:X1,X2,X3:] <> {} ; ::_thesis: ( not [:X1,X2,X3:] = [:Y1,Y2,Y3:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) )
then A2: X3 <> {} by Th31;
 ( X1 <> {} & X2 <> {} ) by A1, Th31;
hence  ( not [:X1,X2,X3:] = [:Y1,Y2,Y3:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 ) ) by A2, Th32; ::_thesis: verum
end;

theorem :: MCART_1:34
for X, Y being set st [:X,X,X:] = [:Y,Y,Y:] holds
X = Y
proof
let X, Y be set ; ::_thesis: ( [:X,X,X:] = [:Y,Y,Y:] implies X = Y )
assume  [:X,X,X:] = [:Y,Y,Y:] ; ::_thesis: X = Y
then  ( ( X <> {} or Y <> {} ) implies X = Y ) by Th32;
hence  X = Y ; ::_thesis: verum
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
let X1, X2, X3 be set ; ::_thesis: ( X1 <> {} & X2 <> {} & X3 <> {} implies 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] )
assume that
A1: ( X1 <> {} & X2 <> {} ) and
A2: X3 <> {} ; ::_thesis: 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]
let x be Element of [:X1,X2,X3:]; ::_thesis: ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
reconsider x9 = x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def_3;
consider x12 being Element of [:X1,X2:], xx3 being Element of X3 such that
A3: x9 = [x12,xx3] by A1, A2, Lm1;
consider xx1 being Element of X1, xx2 being Element of X2 such that
A4: x12 = [xx1,xx2] by A1, Lm1;
take  xx1 ; ::_thesis: ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
take  xx2 ; ::_thesis: ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
take  xx3 ; ::_thesis: x = [xx1,xx2,xx3]
thus  x = [xx1,xx2,xx3] by A3, A4; ::_thesis: verum
end;

theorem Th35: :: MCART_1:35
for x1, x2, x3 being set holds [:{x1},{x2},{x3}:] = {[x1,x2,x3]}
proof
let x1, x2, x3 be set ; ::_thesis: [:{x1},{x2},{x3}:] = {[x1,x2,x3]}
thus [:{x1},{x2},{x3}:] = [:[:{x1},{x2}:],{x3}:] by ZFMISC_1:def_3
.= [:{[x1,x2]},{x3}:] by ZFMISC_1:29
.= {[x1,x2,x3]} by ZFMISC_1:29 ; ::_thesis: verum
end;

theorem :: MCART_1:36
for x1, y1, x2, x3 being set holds [:{x1,y1},{x2},{x3}:] = {[x1,x2,x3],[y1,x2,x3]}
proof
let x1, y1, x2, x3 be set ; ::_thesis: [:{x1,y1},{x2},{x3}:] = {[x1,x2,x3],[y1,x2,x3]}
thus [:{x1,y1},{x2},{x3}:] = [:[:{x1,y1},{x2}:],{x3}:] by ZFMISC_1:def_3
.= [:{[x1,x2],[y1,x2]},{x3}:] by ZFMISC_1:30
.= {[x1,x2,x3],[y1,x2,x3]} by ZFMISC_1:30 ; ::_thesis: verum
end;

theorem :: MCART_1:37
for x1, x2, y2, x3 being set holds [:{x1},{x2,y2},{x3}:] = {[x1,x2,x3],[x1,y2,x3]}
proof
let x1, x2, y2, x3 be set ; ::_thesis: [:{x1},{x2,y2},{x3}:] = {[x1,x2,x3],[x1,y2,x3]}
thus [:{x1},{x2,y2},{x3}:] = [:[:{x1},{x2,y2}:],{x3}:] by ZFMISC_1:def_3
.= [:{[x1,x2],[x1,y2]},{x3}:] by ZFMISC_1:30
.= {[x1,x2,x3],[x1,y2,x3]} by ZFMISC_1:30 ; ::_thesis: verum
end;

theorem :: MCART_1:38
for x1, x2, x3, y3 being set holds [:{x1},{x2},{x3,y3}:] = {[x1,x2,x3],[x1,x2,y3]}
proof
let x1, x2, x3, y3 be set ; ::_thesis: [:{x1},{x2},{x3,y3}:] = {[x1,x2,x3],[x1,x2,y3]}
thus [:{x1},{x2},{x3,y3}:] = [:[:{x1},{x2}:],{x3,y3}:] by ZFMISC_1:def_3
.= [:{[x1,x2]},{x3,y3}:] by ZFMISC_1:29
.= {[x1,x2,x3],[x1,x2,y3]} by ZFMISC_1:30 ; ::_thesis: verum
end;

theorem :: MCART_1:39
for x1, y1, x2, y2, x3 being set holds [:{x1,y1},{x2,y2},{x3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3]}
proof
let x1, y1, x2, y2, x3 be set ; ::_thesis: [:{x1,y1},{x2,y2},{x3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3]}
thus [:{x1,y1},{x2,y2},{x3}:] = [:[:{x1,y1},{x2,y2}:],{x3}:] by ZFMISC_1:def_3
.= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3}:] by Th23
.= [:({[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]}),{x3}:] by ENUMSET1:5
.= [:{[x1,x2],[x1,y2]},{x3}:] \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:97
.= {[[x1,x2],x3],[[x1,y2],x3]} \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:30
.= {[[x1,x2],x3],[[x1,y2],x3]} \/ {[[y1,x2],x3],[[y1,y2],x3]} by ZFMISC_1:30
.= {[x1,x2,x3],[x1,y2,x3],[y1,x2,x3],[[y1,y2],x3]} by ENUMSET1:5
.= {[x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3]} by ENUMSET1:62 ; ::_thesis: verum
end;

theorem :: MCART_1:40
for x1, y1, x2, x3, y3 being set holds [:{x1,y1},{x2},{x3,y3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3]}
proof
let x1, y1, x2, x3, y3 be set ; ::_thesis: [:{x1,y1},{x2},{x3,y3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3]}
thus [:{x1,y1},{x2},{x3,y3}:] = [:[:{x1,y1},{x2}:],{x3,y3}:] by ZFMISC_1:def_3
.= [:{[x1,x2],[y1,x2]},{x3,y3}:] by ZFMISC_1:30
.= {[[x1,x2],x3],[[x1,x2],y3],[[y1,x2],x3],[[y1,x2],y3]} by Th23
.= {[x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3]} by ENUMSET1:62 ; ::_thesis: verum
end;

theorem :: MCART_1:41
for x1, x2, y2, x3, y3 being set holds [:{x1},{x2,y2},{x3,y3}:] = {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]}
proof
let x1, x2, y2, x3, y3 be set ; ::_thesis: [:{x1},{x2,y2},{x3,y3}:] = {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]}
thus [:{x1},{x2,y2},{x3,y3}:] = [:[:{x1},{x2,y2}:],{x3,y3}:] by ZFMISC_1:def_3
.= [:{[x1,x2],[x1,y2]},{x3,y3}:] by ZFMISC_1:30
.= {[[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3]} by Th23
.= {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} by ENUMSET1:62 ; ::_thesis: verum
end;

theorem :: MCART_1:42
for x1, y1, x2, y2, x3, y3 being set holds [:{x1,y1},{x2,y2},{x3,y3}:] = {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3],[y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]}
proof
let x1, y1, x2, y2, x3, y3 be set ; ::_thesis: [:{x1,y1},{x2,y2},{x3,y3}:] = {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3],[y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]}
A1: [:{[x1,x2],[x1,y2]},{x3,y3}:] = {[[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3]} by Th23
.= {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} by ENUMSET1:62 ;
A2: [:{[y1,x2],[y1,y2]},{x3,y3}:] = {[[y1,x2],x3],[[y1,x2],y3],[[y1,y2],x3],[[y1,y2],y3]} by Th23
.= {[y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by ENUMSET1:62 ;
thus [:{x1,y1},{x2,y2},{x3,y3}:] = [:[:{x1,y1},{x2,y2}:],{x3,y3}:] by ZFMISC_1:def_3
.= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3,y3}:] by Th23
.= [:({[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]}),{x3,y3}:] by ENUMSET1:5
.= {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} \/ {[y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by A1, A2, ZFMISC_1:97
.= {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3],[y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by ENUMSET1:25 ; ::_thesis: verum
end;

registration
let X1, X2, X3 be non empty set ;
cluster  ->  triple for Element of [:X1,X2,X3:];
coherence
 for b1 being Element of [:X1,X2,X3:] holds b1 is triple
proof
let x be Element of [:X1,X2,X3:]; ::_thesis: x is triple
 ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3] by Lm2;
hence  x is triple ; ::_thesis: verum
end;
end;

definition
canceled;
canceled;
canceled;
canceled;
let X1, X2, X3 be non empty set ;
let x be Element of [:X1,X2,X3:];
:: original: `1_3
redefine funcx `1_3  ->  Element of X1 means :Def5: :: MCART_1:def 5
 for x1, x2, x3 being set st x = [x1,x2,x3] holds
it = x1;
coherence
 x `1_3 is Element of X1
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
 [xx1,xx2,xx3] `1_3 = xx1 ;
hence  x `1_3 is Element of X1 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X1 holds
( b1 = x `1_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x1 )
proof
let y be Element of X1; ::_thesis: ( y = x `1_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x1 )
thus  ( y = x `1_3 implies for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x1 ) ::_thesis: ( ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x1 ) implies y = x `1_3 )
proof
assume Z: y = x `1_3 ; ::_thesis: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x1
let x1, x2, x3 be set ; ::_thesis: ( x = [x1,x2,x3] implies y = x1 )
assume W: x = [x1,x2,x3] ; ::_thesis: y = x1
 [x1,x2,x3] `1_3 = x1 ;
hence  y = x1 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x1 ; ::_thesis: y = x `1_3
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
 [xx1,xx2,xx3] `1_3 = xx1 ;
hence  y = x `1_3 by Z, A6; ::_thesis: verum
end;
:: original: `2_3
redefine funcx `2_3  ->  Element of X2 means :Def6: :: MCART_1:def 6
 for x1, x2, x3 being set st x = [x1,x2,x3] holds
it = x2;
coherence
 x `2_3 is Element of X2
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
 [xx1,xx2,xx3] `2_3 = xx2 ;
hence  x `2_3 is Element of X2 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X2 holds
( b1 = x `2_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x2 )
proof
let y be Element of X2; ::_thesis: ( y = x `2_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 )
thus  ( y = x `2_3 implies for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ) ::_thesis: ( ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ) implies y = x `2_3 )
proof
assume Z: y = x `2_3 ; ::_thesis: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2
let x1, x2, x3 be set ; ::_thesis: ( x = [x1,x2,x3] implies y = x2 )
assume W: x = [x1,x2,x3] ; ::_thesis: y = x2
 [x1,x2,x3] `2_3 = x2 ;
hence  y = x2 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ; ::_thesis: y = x `2_3
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
 [xx1,xx2,xx3] `2_3 = xx2 ;
hence  y = x `2_3 by Z, A6; ::_thesis: verum
end;
:: original: `2
redefine funcx `3_3  ->  Element of X3 means :Def7: :: MCART_1:def 7
 for x1, x2, x3 being set st x = [x1,x2,x3] holds
it = x3;
coherence
 x `2 is Element of X3
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
 [xx1,xx2,xx3] `3_3 = xx3 ;
hence  x `3_3 is Element of X3 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X3 holds
( b1 = x `2 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x3 )
proof
let y be Element of X3; ::_thesis: ( y = x `2 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x3 )
thus  ( y = x `3_3 implies for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x3 ) ::_thesis: ( ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x3 ) implies y = x `2 )
proof
assume Z: y = x `3_3 ; ::_thesis: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x3
let x1, x2, x3 be set ; ::_thesis: ( x = [x1,x2,x3] implies y = x3 )
assume W: x = [x1,x2,x3] ; ::_thesis: y = x3
 [x1,x2,x3] `3_3 = x3 ;
hence  y = x3 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x3 ; ::_thesis: y = x `2
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
 [xx1,xx2,xx3] `3_3 = xx3 ;
hence  y = x `3_3 by Z, A6; ::_thesis: verum
end;
end;

:: deftheorem  MCART_1:def_1_:_
canceled;

:: deftheorem  MCART_1:def_2_:_
canceled;

:: deftheorem  MCART_1:def_3_:_
canceled;

:: deftheorem  MCART_1:def_4_:_
canceled;

:: deftheorem Def5 defines `1_3 MCART_1:def_5_:_
 for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:]
for b5 being Element of X1 holds
( b5 = x `1_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b5 = x1 );

:: deftheorem Def6 defines `2_3 MCART_1:def_6_:_
 for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:]
for b5 being Element of X2 holds
( b5 = x `2_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b5 = x2 );

:: deftheorem Def7 defines `3_3 MCART_1:def_7_:_
 for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:]
for b5 being Element of X3 holds
( b5 = x `3_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b5 = x3 );

theorem :: MCART_1:43
canceled;

theorem :: MCART_1:44
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds x = [(x `1_3),(x `2_3),(x `3_3)] ;

theorem Th45: :: MCART_1:45
for X, Y, Z being set st ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) holds
X = {}
proof
let X, Y, Z be set ; ::_thesis: ( ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) implies X = {} )
assume that
A1: ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) and
A2: X <> {} ; ::_thesis: contradiction
 ( [:X,Y,Z:] <> {} or [:Y,Z,X:] <> {} or [:Z,X,Y:] <> {} ) by A1, A2;
then reconsider X = X, Y = Y, Z = Z as non empty set by Th31;
percases ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) by A1;
supposeA4: X c= [:X,Y,Z:] ; ::_thesis: contradiction
consider v being set  such that
A5: v in X and
A6: for x, y, z being set st ( x in X or y in X ) holds
v <> [x,y,z] by Th26;
reconsider v = v as Element of [:X,Y,Z:] by A4, A5;
 v = [(v `1_3),(v `2_3),(v `3_3)] ;
hence  contradiction by A6; ::_thesis: verum
end;
suppose X c= [:Y,Z,X:] ; ::_thesis: contradiction
then  X c= [:[:Y,Z:],X:] by ZFMISC_1:def_3;
hence  contradiction by ZFMISC_1:111; ::_thesis: verum
end;
supposeA7: X c= [:Z,X,Y:] ; ::_thesis: contradiction
consider v being set  such that
A8: v in X and
A9: for z, x, y being set st ( z in X or x in X ) holds
v <> [z,x,y] by Th26;
reconsider v = v as Element of [:Z,X,Y:] by A7, A8;
 v = [(v `1_3),(v `2_3),(v `3_3)] ;
hence  contradiction by A9; ::_thesis: verum
end;
end;
end;

theorem :: MCART_1:46
canceled;

theorem Th47: :: MCART_1:47
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )
proof
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] holds
( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )
let x be Element of [:X1,X2,X3:]; ::_thesis: ( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )
set Y9 = {(x `1_3),(x `2_3)};
set Y = {{(x `1_3),(x `2_3)},{(x `1_3)}};
set X9 = {{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)};
set X = {{{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)},{{{(x `1_3),(x `2_3)},{(x `1_3)}}}};
A2: x = [(x `1_3),(x `2_3),(x `3_3)]
.= [[(x `1_3),(x `2_3)],(x `3_3)] ;
then  ( ( x = x `1_3 or x = x `2_3 ) implies ( {{{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)},{{{(x `1_3),(x `2_3)},{(x `1_3)}}}} in {(x `1_3),(x `2_3)} & {(x `1_3),(x `2_3)} in {{(x `1_3),(x `2_3)},{(x `1_3)}} & {{(x `1_3),(x `2_3)},{(x `1_3)}} in {{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)} & {{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)} in {{{{(x `1_3),(x `2_3)},{(x `1_3)}},(x `3_3)},{{{(x `1_3),(x `2_3)},{(x `1_3)}}}} ) ) by TARSKI:def_2;
hence  ( x <> x `1_3 & x <> x `2_3 ) by XREGULAR:8; ::_thesis: x <> x `3_3
thus  x <> x `3_3 by A2, Th20; ::_thesis: verum
end;

theorem :: MCART_1:48
for X1, X2, X3, Y1, Y2, Y3 being set st [:X1,X2,X3:] meets [:Y1,Y2,Y3:] holds
( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 )
proof
let X1, X2, X3, Y1, Y2, Y3 be set ; ::_thesis: ( [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies ( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 ) )
assume A1: [:X1,X2,X3:] meets [:Y1,Y2,Y3:] ; ::_thesis: ( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 )
A2: ( [:[:X1,X2:],X3:] = [:X1,X2,X3:] & [:[:Y1,Y2:],Y3:] = [:Y1,Y2,Y3:] ) by ZFMISC_1:def_3;
then  [:X1,X2:] meets [:Y1,Y2:] by A1, ZFMISC_1:104;
hence  ( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 ) by A2, A1, ZFMISC_1:104; ::_thesis: verum
end;

theorem Th49: :: MCART_1:49
for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
proof
let X1, X2, X3, X4 be set ; ::_thesis: [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
thus [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def_4
.= [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def_3 ; ::_thesis: verum
end;

theorem Th50: :: MCART_1:50
for X1, X2, X3, X4 being set holds [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
proof
let X1, X2, X3, X4 be set ; ::_thesis: [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
thus [:[:X1,X2:],X3,X4:] = [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def_3
.= [:X1,X2,X3,X4:] by Th49 ; ::_thesis: verum
end;

theorem Th51: :: MCART_1:51
for X1, X2, X3, X4 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
proof
let X1, X2, X3, X4 be set ; ::_thesis: ( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
A1: [:[:X1,X2,X3:],X4:] = [:X1,X2,X3,X4:] by ZFMISC_1:def_4;
 ( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} ) by Th31;
hence  ( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} ) by A1, ZFMISC_1:90; ::_thesis: verum
end;

theorem Th52: :: MCART_1:52
for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )
proof
let X1, X2, X3, X4, Y1, Y2, Y3, Y4 be set ; ::_thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def_4;
assume A2: ( X1 <> {} & X2 <> {} & X3 <> {} ) ; ::_thesis: ( not X4 <> {} or not [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
assume A3: X4 <> {} ; ::_thesis: ( not [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
assume  [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] ; ::_thesis: ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )
then A4: [:[:X1,X2,X3:],X4:] = [:[:Y1,Y2,Y3:],Y4:] by A1, ZFMISC_1:def_4;
 [:X1,X2,X3:] = [:Y1,Y2,Y3:] by A3, A4, A2, ZFMISC_1:110;
hence  ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) by A2, A3, A4, Th32, ZFMISC_1:110; ::_thesis: verum
end;

theorem :: MCART_1:53
for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st [:X1,X2,X3,X4:] <> {} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )
proof
let X1, X2, X3, X4, Y1, Y2, Y3, Y4 be set ; ::_thesis: ( [:X1,X2,X3,X4:] <> {} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
assume A1: [:X1,X2,X3,X4:] <> {} ; ::_thesis: ( not [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) )
then A2: ( X3 <> {} & X4 <> {} ) by Th51;
 ( X1 <> {} & X2 <> {} ) by A1, Th51;
hence  ( not [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] or ( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 ) ) by A2, Th52; ::_thesis: verum
end;

theorem :: MCART_1:54
for X, Y being set st [:X,X,X,X:] = [:Y,Y,Y,Y:] holds
X = Y
proof
let X, Y be set ; ::_thesis: ( [:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y )
assume  [:X,X,X,X:] = [:Y,Y,Y,Y:] ; ::_thesis: X = Y
then  ( ( X <> {} or Y <> {} ) implies X = Y ) by Th52;
hence  X = Y ; ::_thesis: verum
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
let X1, X2, X3, X4 be set ; ::_thesis: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies 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] )
assume that
A1: ( X1 <> {} & X2 <> {} & X3 <> {} ) and
A2: X4 <> {} ; ::_thesis: 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]
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: 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]
reconsider x9 = x as Element of [:[:X1,X2,X3:],X4:] by ZFMISC_1:def_4;
consider x123 being Element of [:X1,X2,X3:], xx4 being Element of X4 such that
A3: x9 = [x123,xx4] by A2, Lm1, A1;
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A4: x123 = [xx1,xx2,xx3] by A1, Lm2;
take  xx1 ; ::_thesis: ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]
take  xx2 ; ::_thesis: ex xx3 being Element of X3 ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]
take  xx3 ; ::_thesis: ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]
take  xx4 ; ::_thesis: x = [xx1,xx2,xx3,xx4]
thus  x = [xx1,xx2,xx3,xx4] by A3, A4; ::_thesis: verum
end;

registration
let X1, X2, X3, X4 be non empty set ;
cluster  ->  quadruple for Element of [:X1,X2,X3,X4:];
coherence
 for b1 being Element of [:X1,X2,X3,X4:] holds b1 is quadruple
proof
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: x is quadruple
 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] by Lm3;
hence  x is quadruple ; ::_thesis: verum
end;
end;

definition
let X1, X2, X3, X4 be non empty set ;
let x be Element of [:X1,X2,X3,X4:];
:: original: `1_4
redefine funcx `1_4  ->  Element of X1 means :Def8: :: MCART_1:def 8
 for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
it = x1;
coherence
 x `1_4 is Element of X1
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `1_4 = xx1 ;
hence  x `1_4 is Element of X1 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X1 holds
( b1 = x `1_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x1 )
proof
let y be Element of X1; ::_thesis: ( y = x `1_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 )
thus  ( y = x `1_4 implies for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 ) ::_thesis: ( ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 ) implies y = x `1_4 )
proof
assume Z: y = x `1_4 ; ::_thesis: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1
let x1, x2, x3, x4 be set ; ::_thesis: ( x = [x1,x2,x3,x4] implies y = x1 )
assume W: x = [x1,x2,x3,x4] ; ::_thesis: y = x1
 [x1,x2,x3,x4] `1_4 = x1 ;
hence  y = x1 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x1 ; ::_thesis: y = x `1_4
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `1_4 = xx1 ;
hence  y = x `1_4 by Z, A6; ::_thesis: verum
end;
:: original: `2_4
redefine funcx `2_4  ->  Element of X2 means :Def9: :: MCART_1:def 9
 for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
it = x2;
coherence
 x `2_4 is Element of X2
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `2_4 = xx2 ;
hence  x `2_4 is Element of X2 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X2 holds
( b1 = x `2_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x2 )
proof
let y be Element of X2; ::_thesis: ( y = x `2_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x2 )
thus  ( y = x `2_4 implies for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x2 ) ::_thesis: ( ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x2 ) implies y = x `2_4 )
proof
assume Z: y = x `2_4 ; ::_thesis: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x2
let x1, x2, x3, x4 be set ; ::_thesis: ( x = [x1,x2,x3,x4] implies y = x2 )
assume W: x = [x1,x2,x3,x4] ; ::_thesis: y = x2
 [x1,x2,x3,x4] `2_4 = x2 ;
hence  y = x2 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x2 ; ::_thesis: y = x `2_4
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `2_4 = xx2 ;
hence  y = x `2_4 by Z, A6; ::_thesis: verum
end;
:: original: `2_3
redefine funcx `3_4  ->  Element of X3 means :Def10: :: MCART_1:def 10
 for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
it = x3;
coherence
 x `2_3 is Element of X3
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `3_4 = xx3 ;
hence  x `3_4 is Element of X3 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X3 holds
( b1 = x `2_3 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x3 )
proof
let y be Element of X3; ::_thesis: ( y = x `2_3 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x3 )
thus  ( y = x `3_4 implies for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x3 ) ::_thesis: ( ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x3 ) implies y = x `2_3 )
proof
assume Z: y = x `3_4 ; ::_thesis: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x3
let x1, x2, x3, x4 be set ; ::_thesis: ( x = [x1,x2,x3,x4] implies y = x3 )
assume W: x = [x1,x2,x3,x4] ; ::_thesis: y = x3
 [x1,x2,x3,x4] `3_4 = x3 ;
hence  y = x3 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x3 ; ::_thesis: y = x `2_3
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `3_4 = xx3 ;
hence  y = x `3_4 by Z, A6; ::_thesis: verum
end;
:: original: `2
redefine funcx `4_4  ->  Element of X4 means :Def11: :: MCART_1:def 11
 for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
it = x4;
coherence
 x `2 is Element of X4
proof
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `4_4 = xx4 ;
hence  x `4_4 is Element of X4 by A6; ::_thesis: verum
end;
compatibility
 for b1 being Element of X4 holds
( b1 = x `2 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x4 )
proof
let y be Element of X4; ::_thesis: ( y = x `2 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x4 )
thus  ( y = x `4_4 implies for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x4 ) ::_thesis: ( ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x4 ) implies y = x `2 )
proof
assume Z: y = x `4_4 ; ::_thesis: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x4
let x1, x2, x3, x4 be set ; ::_thesis: ( x = [x1,x2,x3,x4] implies y = x4 )
assume W: x = [x1,x2,x3,x4] ; ::_thesis: y = x4
 [x1,x2,x3,x4] `4_4 = x4 ;
hence  y = x4 by W, Z; ::_thesis: verum
end;
assume Z: for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
y = x4 ; ::_thesis: y = x `2
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
 [xx1,xx2,xx3,xx4] `4_4 = xx4 ;
hence  y = x `4_4 by Z, A6; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines `1_4 MCART_1:def_8_:_
 for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X1 holds
( b6 = x `1_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x1 );

:: deftheorem Def9 defines `2_4 MCART_1:def_9_:_
 for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X2 holds
( b6 = x `2_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x2 );

:: deftheorem Def10 defines `3_4 MCART_1:def_10_:_
 for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X3 holds
( b6 = x `3_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x3 );

:: deftheorem Def11 defines `4_4 MCART_1:def_11_:_
 for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X4 holds
( b6 = x `4_4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x4 );

theorem :: MCART_1:55
canceled;

theorem :: MCART_1:56
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;

theorem :: MCART_1:57
canceled;

theorem :: MCART_1:58
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )
proof
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] holds
( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( x <> x `1_4 & x <> x `2_4 & x <> x `3_4 & x <> x `4_4 )
reconsider Y = [:X1,X2:], X3 = X3, X4 = X4 as non empty set ;
reconsider x9 = x as Element of [:Y,X3,X4:] by Th50;
set Z9 = {(x `1_4),(x `2_4)};
set Z = {{(x `1_4),(x `2_4)},{(x `1_4)}};
set Y9 = {{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)};
set Y = {{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}};
set X9 = {{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)};
set X = {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}};
x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)]
.= {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}} ;
then  ( ( x = x `1_4 or x = x `2_4 ) implies ( {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}} in {(x `1_4),(x `2_4)} & {(x `1_4),(x `2_4)} in {{(x `1_4),(x `2_4)},{(x `1_4)}} & {{(x `1_4),(x `2_4)},{(x `1_4)}} in {{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)} & {{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)} in {{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}} & {{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}} in {{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)} & {{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)} in {{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}},(x `4_4)},{{{{{(x `1_4),(x `2_4)},{(x `1_4)}},(x `3_4)},{{{(x `1_4),(x `2_4)},{(x `1_4)}}}}}} ) ) by TARSKI:def_2;
hence  ( x <> x `1_4 & x <> x `2_4 ) by XREGULAR:10; ::_thesis: ( x <> x `3_4 & x <> x `4_4 )
x `3_4 = (x `1) `2
.= x9 `2_3 ;
hence  ( x <> x `3_4 & x <> x `4_4 ) by Th47; ::_thesis: verum
end;

theorem :: MCART_1:59
for X1, X2, X3, X4 being set st ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) holds
X1 = {}
proof
let X1, X2, X3, X4 be set ; ::_thesis: ( ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) implies X1 = {} )
assume that
A1: ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) and
A2: X1 <> {} ; ::_thesis: contradiction
A3: ( [:X1,X2,X3,X4:] <> {} or [:X2,X3,X4,X1:] <> {} or [:X3,X4,X1,X2:] <> {} or [:X4,X1,X2,X3:] <> {} ) by A1, A2;
reconsider X1 = X1, X2 = X2, X3 = X3, X4 = X4 as non empty set by A3, Th51;
percases ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) by A1;
supposeA6: X1 c= [:X1,X2,X3,X4:] ; ::_thesis: contradiction
consider v being set  such that
A7: v in X1 and
A8: for x1, x2, x3, x4 being set st ( x1 in X1 or x2 in X1 ) holds
v <> [x1,x2,x3,x4] by Th30;
reconsider v = v as Element of [:X1,X2,X3,X4:] by A6, A7;
 v = [(v `1_4),(v `2_4),(v `3_4),(v `4_4)] ;
hence  contradiction by A8; ::_thesis: verum
end;
suppose X1 c= [:X2,X3,X4,X1:] ; ::_thesis: contradiction
then  X1 c= [:[:X2,X3:],X4,X1:] by Th50;
hence  contradiction by Th45; ::_thesis: verum
end;
suppose X1 c= [:X3,X4,X1,X2:] ; ::_thesis: contradiction
then  X1 c= [:[:X3,X4:],X1,X2:] by Th50;
hence  contradiction by Th45; ::_thesis: verum
end;
supposeA9: X1 c= [:X4,X1,X2,X3:] ; ::_thesis: contradiction
consider v being set  such that
A10: v in X1 and
A11: for x1, x2, x3, x4 being set st ( x1 in X1 or x2 in X1 ) holds
v <> [x1,x2,x3,x4] by Th30;
reconsider v = v as Element of [:X4,X1,X2,X3:] by A9, A10;
 v = [(v `1_4),(v `2_4),(v `3_4),(v `4_4)] ;
hence  contradiction by A11; ::_thesis: verum
end;
end;
end;

theorem :: MCART_1:60
for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] holds
( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 )
proof
let X1, X2, X3, X4, Y1, Y2, Y3, Y4 be set ; ::_thesis: ( [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies ( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 ) )
assume A1: [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] ; ::_thesis: ( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 )
A2: ( [:[:[:X1,X2:],X3:],X4:] = [:X1,X2,X3,X4:] & [:[:[:Y1,Y2:],Y3:],Y4:] = [:Y1,Y2,Y3,Y4:] ) by Th49;
then A3: [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:] by A1, ZFMISC_1:104;
then  [:X1,X2:] meets [:Y1,Y2:] by ZFMISC_1:104;
hence  ( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 ) by A2, A1, A3, ZFMISC_1:104; ::_thesis: verum
end;

theorem :: MCART_1:61
for x1, x2, x3, x4 being set holds [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
proof
let x1, x2, x3, x4 be set ; ::_thesis: [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th50
.= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:29
.= {[[x1,x2],x3,x4]} by Th35
.= {[x1,x2,x3,x4]} ; ::_thesis: verum
end;

theorem Th62: :: MCART_1:62
for X, Y being set st [:X,Y:] <> {} holds
for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
proof
let X, Y be set ; ::_thesis: ( [:X,Y:] <> {} implies for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 ) )
assume  [:X,Y:] <> {} ; ::_thesis: for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
then  ( X <> {} & Y <> {} ) by ZFMISC_1:90;
hence  for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 ) by Th24; ::_thesis: verum
end;

theorem :: MCART_1:63
for x, X, Y being set st x in [:X,Y:] holds
( x <> x `1 & x <> x `2 ) by Th62;


theorem :: MCART_1:64
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:]
for x1, x2, x3 being set st x = [x1,x2,x3] holds
( x `1_3 = x1 & x `2_3 = x2 & x `3_3 = x3 ) by Def5, Def6, Def7;

theorem :: MCART_1:65
for y1 being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y1 = xx1 ) holds
y1 = x `1_3
proof
let y1 be set ; ::_thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y1 = xx1 ) holds
y1 = x `1_3
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y1 = xx1 ) holds
y1 = x `1_3
let x be Element of [:X1,X2,X3:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y1 = xx1 ) implies y1 = x `1_3 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y1 = xx1 ; ::_thesis: y1 = x `1_3
 x = [(x `1_3),(x `2_3),(x `3_3)] ;
hence  y1 = x `1_3 by A2; ::_thesis: verum
end;

theorem :: MCART_1:66
for y2 being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ) holds
y2 = x `2_3
proof
let y2 be set ; ::_thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ) holds
y2 = x `2_3
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ) holds
y2 = x `2_3
let x be Element of [:X1,X2,X3:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ) implies y2 = x `2_3 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y2 = xx2 ; ::_thesis: y2 = x `2_3
 x = [(x `1_3),(x `2_3),(x `3_3)] ;
hence  y2 = x `2_3 by A2; ::_thesis: verum
end;

theorem :: MCART_1:67
for y3 being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) holds
y3 = x `3_3
proof
let y3 be set ; ::_thesis: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) holds
y3 = x `3_3
let X1, X2, X3 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) holds
y3 = x `3_3
let x be Element of [:X1,X2,X3:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ) implies y3 = x `3_3 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3 st x = [xx1,xx2,xx3] holds
y3 = xx3 ; ::_thesis: y3 = x `3_3
 x = [(x `1_3),(x `2_3),(x `3_3)] ;
hence  y3 = x `3_3 by A2; ::_thesis: verum
end;

theorem Th68: :: MCART_1:68
for z, X1, X2, X3 being set st z in [:X1,X2,X3:] holds
ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] )
proof
let z, X1, X2, X3 be set ; ::_thesis: ( z in [:X1,X2,X3:] implies ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) )
assume  z in [:X1,X2,X3:] ; ::_thesis: ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] )
then  z in [:[:X1,X2:],X3:] by ZFMISC_1:def_3;
then consider x12, x3 being set  such that
A1: x12 in [:X1,X2:] and
A2: x3 in X3 and
A3: z = [x12,x3] by ZFMISC_1:def_2;
consider x1, x2 being set  such that
A4: ( x1 in X1 & x2 in X2 ) and
A5: x12 = [x1,x2] by A1, ZFMISC_1:def_2;
 z = [x1,x2,x3] by A3, A5;
hence  ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) by A2, A4; ::_thesis: verum
end;

theorem Th69: :: MCART_1:69
for x1, x2, x3, X1, X2, X3 being set holds
( [x1,x2,x3] in [:X1,X2,X3:] iff ( x1 in X1 & x2 in X2 & x3 in X3 ) )
proof
let x1, x2, x3, X1, X2, X3 be set ; ::_thesis: ( [x1,x2,x3] in [:X1,X2,X3:] iff ( x1 in X1 & x2 in X2 & x3 in X3 ) )
A1: ( [x1,x2] in [:X1,X2:] iff ( x1 in X1 & x2 in X2 ) ) by ZFMISC_1:87;
 [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def_3;
hence  ( [x1,x2,x3] in [:X1,X2,X3:] iff ( x1 in X1 & x2 in X2 & x3 in X3 ) ) by A1, ZFMISC_1:87; ::_thesis: verum
end;

theorem :: MCART_1:70
for Z, X1, X2, X3 being set st ( for z being set holds
( z in Z iff ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) ) ) holds
Z = [:X1,X2,X3:]
proof
let Z, X1, X2, X3 be set ; ::_thesis: ( ( for z being set holds
( z in Z iff ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) ) ) implies Z = [:X1,X2,X3:] )
assume A1: for z being set holds
( z in Z iff ex x1, x2, x3 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) ) ; ::_thesis: Z = [:X1,X2,X3:]
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_Z_implies_z_in_[:[:X1,X2:],X3:]_)_&_(_z_in_[:[:X1,X2:],X3:]_implies_z_in_Z_)_)
let z be set ; ::_thesis: ( ( z in Z implies z in [:[:X1,X2:],X3:] ) & ( z in [:[:X1,X2:],X3:] implies z in Z ) )
thus  ( z in Z implies z in [:[:X1,X2:],X3:] ) ::_thesis: ( z in [:[:X1,X2:],X3:] implies z in Z )
proof
assume  z in Z ; ::_thesis: z in [:[:X1,X2:],X3:]
then consider x1, x2, x3 being set  such that
A2: ( x1 in X1 & x2 in X2 ) and
A3: ( x3 in X3 & z = [x1,x2,x3] ) by A1;
 [x1,x2] in [:X1,X2:] by A2, ZFMISC_1:def_2;
hence  z in [:[:X1,X2:],X3:] by A3, ZFMISC_1:def_2; ::_thesis: verum
end;
assume  z in [:[:X1,X2:],X3:] ; ::_thesis: z in Z
then consider x12, x3 being set  such that
A4: x12 in [:X1,X2:] and
A5: x3 in X3 and
A6: z = [x12,x3] by ZFMISC_1:def_2;
consider x1, x2 being set  such that
A7: ( x1 in X1 & x2 in X2 ) and
A8: x12 = [x1,x2] by A4, ZFMISC_1:def_2;
 z = [x1,x2,x3] by A6, A8;
hence  z in Z by A1, A5, A7; ::_thesis: verum
end;
then  Z = [:[:X1,X2:],X3:] by TARSKI:1;
hence  Z = [:X1,X2,X3:] by ZFMISC_1:def_3; ::_thesis: verum
end;

theorem :: MCART_1:71
canceled;

theorem :: MCART_1:72
for X1, X2, X3 being non empty set
for A1 being non empty Subset of X1
for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )
proof
let X1, X2, X3 be non empty set ; ::_thesis: for A1 being non empty Subset of X1
for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )
let A1 be non empty Subset of X1; ::_thesis: for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )
let A2 be non empty Subset of X2; ::_thesis: for A3 being non empty Subset of X3
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )
let A3 be non empty Subset of X3; ::_thesis: for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )
let x be Element of [:X1,X2,X3:]; ::_thesis: ( x in [:A1,A2,A3:] implies ( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 ) )
assume  x in [:A1,A2,A3:] ; ::_thesis: ( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 )
then reconsider y = x as Element of [:A1,A2,A3:] ;
A2: y `2_3 in A2 ;
A3: y `3_3 in A3 ;
 y `1_3 in A1 ;
hence  ( x `1_3 in A1 & x `2_3 in A2 & x `3_3 in A3 ) by A2, A3; ::_thesis: verum
end;

theorem Th73: :: MCART_1:73
for X1, Y1, X2, Y2, X3, Y3 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 holds
[:X1,X2,X3:] c= [:Y1,Y2,Y3:]
proof
let X1, Y1, X2, Y2, X3, Y3 be set ; ::_thesis: ( X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,Y3:] )
A1: ( [:X1,X2,X3:] = [:[:X1,X2:],X3:] & [:Y1,Y2,Y3:] = [:[:Y1,Y2:],Y3:] ) by ZFMISC_1:def_3;
assume  ( X1 c= Y1 & X2 c= Y2 ) ; ::_thesis: ( not X3 c= Y3 or [:X1,X2,X3:] c= [:Y1,Y2,Y3:] )
then A2: [:X1,X2:] c= [:Y1,Y2:] by ZFMISC_1:96;
assume  X3 c= Y3 ; ::_thesis: [:X1,X2,X3:] c= [:Y1,Y2,Y3:]
hence  [:X1,X2,X3:] c= [:Y1,Y2,Y3:] by A2, A1, ZFMISC_1:96; ::_thesis: verum
end;

theorem :: MCART_1:74
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
( x `1_4 = x1 & x `2_4 = x2 & x `3_4 = x3 & x `4_4 = x4 ) by Def8, Def9, Def10, Def11;

theorem :: MCART_1:75
for y1 being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y1 = xx1 ) holds
y1 = x `1_4
proof
let y1 be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y1 = xx1 ) holds
y1 = x `1_4
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y1 = xx1 ) holds
y1 = x `1_4
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y1 = xx1 ) implies y1 = x `1_4 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y1 = xx1 ; ::_thesis: y1 = x `1_4
 x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence  y1 = x `1_4 by A2; ::_thesis: verum
end;

theorem :: MCART_1:76
for y2 being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y2 = xx2 ) holds
y2 = x `2_4
proof
let y2 be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y2 = xx2 ) holds
y2 = x `2_4
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y2 = xx2 ) holds
y2 = x `2_4
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y2 = xx2 ) implies y2 = x `2_4 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y2 = xx2 ; ::_thesis: y2 = x `2_4
 x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence  y2 = x `2_4 by A2; ::_thesis: verum
end;

theorem :: MCART_1:77
for y3 being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y3 = xx3 ) holds
y3 = x `3_4
proof
let y3 be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y3 = xx3 ) holds
y3 = x `3_4
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y3 = xx3 ) holds
y3 = x `3_4
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y3 = xx3 ) implies y3 = x `3_4 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y3 = xx3 ; ::_thesis: y3 = x `3_4
 x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence  y3 = x `3_4 by A2; ::_thesis: verum
end;

theorem :: MCART_1:78
for y4 being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) holds
y4 = x `4_4
proof
let y4 be set ; ::_thesis: for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) holds
y4 = x `4_4
let X1, X2, X3, X4 be non empty set ; ::_thesis: for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) holds
y4 = x `4_4
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( ( for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ) implies y4 = x `4_4 )
assume A2: for xx1 being Element of X1
for xx2 being Element of X2
for xx3 being Element of X3
for xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds
y4 = xx4 ; ::_thesis: y4 = x `4_4
 x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence  y4 = x `4_4 by A2; ::_thesis: verum
end;

theorem :: MCART_1:79
for z, X1, X2, X3, X4 being set st z in [:X1,X2,X3,X4:] holds
ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] )
proof
let z, X1, X2, X3, X4 be set ; ::_thesis: ( z in [:X1,X2,X3,X4:] implies ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) )
assume  z in [:X1,X2,X3,X4:] ; ::_thesis: ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] )
then  z in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def_4;
then consider x123, x4 being set  such that
A1: x123 in [:X1,X2,X3:] and
A2: x4 in X4 and
A3: z = [x123,x4] by ZFMISC_1:def_2;
consider x1, x2, x3 being set  such that
A4: ( x1 in X1 & x2 in X2 & x3 in X3 ) and
A5: x123 = [x1,x2,x3] by A1, Th68;
 z = [x1,x2,x3,x4] by A3, A5;
hence  ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) by A2, A4; ::_thesis: verum
end;

theorem :: MCART_1:80
for x1, x2, x3, x4, X1, X2, X3, X4 being set holds
( [x1,x2,x3,x4] in [:X1,X2,X3,X4:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 ) )
proof
let x1, x2, x3, x4, X1, X2, X3, X4 be set ; ::_thesis: ( [x1,x2,x3,x4] in [:X1,X2,X3,X4:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 ) )
A1: ( [x1,x2] in [:X1,X2:] iff ( x1 in X1 & x2 in X2 ) ) by ZFMISC_1:87;
 ( [:X1,X2,X3,X4:] = [:[:X1,X2:],X3,X4:] & [x1,x2,x3,x4] = [[x1,x2],x3,x4] ) by Th50;
hence  ( [x1,x2,x3,x4] in [:X1,X2,X3,X4:] iff ( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 ) ) by A1, Th69; ::_thesis: verum
end;

theorem :: MCART_1:81
for Z, X1, X2, X3, X4 being set st ( for z being set holds
( z in Z iff ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) ) ) holds
Z = [:X1,X2,X3,X4:]
proof
let Z, X1, X2, X3, X4 be set ; ::_thesis: ( ( for z being set holds
( z in Z iff ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) ) ) implies Z = [:X1,X2,X3,X4:] )
assume A1: for z being set holds
( z in Z iff ex x1, x2, x3, x4 being set st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] ) ) ; ::_thesis: Z = [:X1,X2,X3,X4:]
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_Z_implies_z_in_[:[:X1,X2,X3:],X4:]_)_&_(_z_in_[:[:X1,X2,X3:],X4:]_implies_z_in_Z_)_)
let z be set ; ::_thesis: ( ( z in Z implies z in [:[:X1,X2,X3:],X4:] ) & ( z in [:[:X1,X2,X3:],X4:] implies z in Z ) )
thus  ( z in Z implies z in [:[:X1,X2,X3:],X4:] ) ::_thesis: ( z in [:[:X1,X2,X3:],X4:] implies z in Z )
proof
assume  z in Z ; ::_thesis: z in [:[:X1,X2,X3:],X4:]
then consider x1, x2, x3, x4 being set  such that
A2: ( x1 in X1 & x2 in X2 & x3 in X3 ) and
A3: ( x4 in X4 & z = [x1,x2,x3,x4] ) by A1;
 [x1,x2,x3] in [:X1,X2,X3:] by A2, Th69;
hence  z in [:[:X1,X2,X3:],X4:] by A3, ZFMISC_1:def_2; ::_thesis: verum
end;
assume  z in [:[:X1,X2,X3:],X4:] ; ::_thesis: z in Z
then consider x123, x4 being set  such that
A4: x123 in [:X1,X2,X3:] and
A5: x4 in X4 and
A6: z = [x123,x4] by ZFMISC_1:def_2;
consider x1, x2, x3 being set  such that
A7: ( x1 in X1 & x2 in X2 & x3 in X3 ) and
A8: x123 = [x1,x2,x3] by A4, Th68;
 z = [x1,x2,x3,x4] by A6, A8;
hence  z in Z by A1, A5, A7; ::_thesis: verum
end;
then  Z = [:[:X1,X2,X3:],X4:] by TARSKI:1;
hence  Z = [:X1,X2,X3,X4:] by ZFMISC_1:def_4; ::_thesis: verum
end;

theorem :: MCART_1:82
canceled;

theorem :: MCART_1:83
for X1, X2, X3, X4 being non empty set
for A1 being non empty Subset of X1
for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
proof
let X1, X2, X3, X4 be non empty set ; ::_thesis: for A1 being non empty Subset of X1
for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
let A1 be non empty Subset of X1; ::_thesis: for A2 being non empty Subset of X2
for A3 being non empty Subset of X3
for A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
let A2 be non empty Subset of X2; ::_thesis: for A3 being non empty Subset of X3
for A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
let A3 be non empty Subset of X3; ::_thesis: for A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
let A4 be non empty Subset of X4; ::_thesis: for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
let x be Element of [:X1,X2,X3,X4:]; ::_thesis: ( x in [:A1,A2,A3,A4:] implies ( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 ) )
assume  x in [:A1,A2,A3,A4:] ; ::_thesis: ( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 )
then reconsider y = x as Element of [:A1,A2,A3,A4:] ;
A2: y `2_4 in A2 ;
A3: y `4_4 in A4 ;
A4: y `3_4 in A3 ;
 y `1_4 in A1 ;
hence  ( x `1_4 in A1 & x `2_4 in A2 & x `3_4 in A3 & x `4_4 in A4 ) by A2, A4, A3; ::_thesis: verum
end;

theorem Th84: :: MCART_1:84
for X1, Y1, X2, Y2, X3, Y3, X4, Y4 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 holds
[:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]
proof
let X1, Y1, X2, Y2, X3, Y3, X4, Y4 be set ; ::_thesis: ( X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] )
A1: ( [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] & [:Y1,Y2,Y3,Y4:] = [:[:Y1,Y2,Y3:],Y4:] ) by ZFMISC_1:def_4;
assume  ( X1 c= Y1 & X2 c= Y2 & X3 c= Y3 ) ; ::_thesis: ( not X4 c= Y4 or [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] )
then A2: [:X1,X2,X3:] c= [:Y1,Y2,Y3:] by Th73;
assume  X4 c= Y4 ; ::_thesis: [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]
hence  [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:] by A2, A1, ZFMISC_1:96; ::_thesis: verum
end;

definition
let X1, X2 be set ;
let A1 be Subset of X1;
let A2 be Subset of X2;
:: original: [:
redefine func[:A1,A2:] ->  Subset of [:X1,X2:];
coherence
 [:A1,A2:] is Subset of [:X1,X2:] by ZFMISC_1:96;
end;

definition
let X1, X2, X3 be set ;
let A1 be Subset of X1;
let A2 be Subset of X2;
let A3 be Subset of X3;
:: original: [:
redefine func[:A1,A2,A3:] ->  Subset of [:X1,X2,X3:];
coherence
 [:A1,A2,A3:] is Subset of [:X1,X2,X3:] by Th73;
end;

definition
let X1, X2, X3, X4 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;
:: original: [:
redefine func[:A1,A2,A3,A4:] ->  Subset of [:X1,X2,X3,X4:];
coherence
 [:A1,A2,A3,A4:] is Subset of [:X1,X2,X3,X4:] by Th84;
end;

begin

definition
let f be Function;
func pr1 f ->  Function means :: MCART_1:def 12
( dom it = dom f & ( for x being set st x in dom f holds
it . x = (f . x) `1 ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = (f . x) `1 ) )
proof
deffunc H1( set ) ->  set = (f . $1) `1 ;
 ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = (f . x) `1 ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = (f . x) `1 ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = (f . x) `1 ) holds
b1 = b2
proof
let p1, p2 be Function; ::_thesis: ( dom p1 = dom f & ( for x being set st x in dom f holds
p1 . x = (f . x) `1 ) & dom p2 = dom f & ( for x being set st x in dom f holds
p2 . x = (f . x) `1 ) implies p1 = p2 )
assume that
A1: dom p1 = dom f and
A2: for x being set st x in dom f holds
p1 . x = (f . x) `1 and
A3: dom p2 = dom f and
A4: for x being set st x in dom f holds
p2 . x = (f . x) `1 ; ::_thesis: p1 = p2
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
p1_._x_=_p2_._x
let x be set ; ::_thesis: ( x in dom f implies p1 . x = p2 . x )
assume A5: x in dom f ; ::_thesis: p1 . x = p2 . x
then  p1 . x = (f . x) `1 by A2;
hence  p1 . x = p2 . x by A4, A5; ::_thesis: verum
end;
hence  p1 = p2 by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
func pr2 f ->  Function means :: MCART_1:def 13
( dom it = dom f & ( for x being set st x in dom f holds
it . x = (f . x) `2 ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = (f . x) `2 ) )
proof
deffunc H1( set ) ->  set = (f . $1) `2 ;
 ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = (f . x) `2 ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = (f . x) `2 ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = (f . x) `2 ) holds
b1 = b2
proof
let p1, p2 be Function; ::_thesis: ( dom p1 = dom f & ( for x being set st x in dom f holds
p1 . x = (f . x) `2 ) & dom p2 = dom f & ( for x being set st x in dom f holds
p2 . x = (f . x) `2 ) implies p1 = p2 )
assume that
A6: dom p1 = dom f and
A7: for x being set st x in dom f holds
p1 . x = (f . x) `2 and
A8: dom p2 = dom f and
A9: for x being set st x in dom f holds
p2 . x = (f . x) `2 ; ::_thesis: p1 = p2
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
p1_._x_=_p2_._x
let x be set ; ::_thesis: ( x in dom f implies p1 . x = p2 . x )
assume A10: x in dom f ; ::_thesis: p1 . x = p2 . x
then  p1 . x = (f . x) `2 by A7;
hence  p1 . x = p2 . x by A9, A10; ::_thesis: verum
end;
hence  p1 = p2 by A6, A8, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines pr1 MCART_1:def_12_:_
 for f, b2 being Function holds
( b2 = pr1 f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = (f . x) `1 ) ) );

:: deftheorem  defines pr2 MCART_1:def_13_:_
 for f, b2 being Function holds
( b2 = pr2 f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = (f . x) `2 ) ) );

definition
let x be set ;
funcx `11  ->  set  equals :: MCART_1:def 14
(x `1) `1 ;
coherence
 (x `1) `1 is set ;
funcx `12  ->  set  equals :: MCART_1:def 15
(x `1) `2 ;
coherence
 (x `1) `2 is set ;
funcx `21  ->  set  equals :: MCART_1:def 16
(x `2) `1 ;
coherence
 (x `2) `1 is set ;
funcx `22  ->  set  equals :: MCART_1:def 17
(x `2) `2 ;
coherence
 (x `2) `2 is set ;
end;

:: deftheorem  defines `11 MCART_1:def_14_:_
 for x being set holds x `11 = (x `1) `1 ;

:: deftheorem  defines `12 MCART_1:def_15_:_
 for x being set holds x `12 = (x `1) `2 ;

:: deftheorem  defines `21 MCART_1:def_16_:_
 for x being set holds x `21 = (x `2) `1 ;

:: deftheorem  defines `22 MCART_1:def_17_:_
 for x being set holds x `22 = (x `2) `2 ;

theorem :: MCART_1:85
for x1, x2, y, y1, y2, x being set holds
( [[x1,x2],y] `11 = x1 & [[x1,x2],y] `12 = x2 & [x,[y1,y2]] `21 = y1 & [x,[y1,y2]] `22 = y2 ) ;

theorem :: MCART_1:86
for R being Relation
for x being set st x in R holds
( x `1 in dom R & x `2 in rng R )
proof
let R be Relation; ::_thesis: for x being set st x in R holds
( x `1 in dom R & x `2 in rng R )
let x be set ; ::_thesis: ( x in R implies ( x `1 in dom R & x `2 in rng R ) )
assume A1: x in R ; ::_thesis: ( x `1 in dom R & x `2 in rng R )
then  x = [(x `1),(x `2)] by Th21;
hence  ( x `1 in dom R & x `2 in rng R ) by A1, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th87: :: MCART_1:87
for R being non empty Relation
for x being set holds Im (R,x) =  {  (I `2) where I is Element of R : I `1 = x  }
proof
let R be non empty Relation; ::_thesis: for x being set holds Im (R,x) =  {  (I `2) where I is Element of R : I `1 = x  }
let x be set ; ::_thesis: Im (R,x) =  {  (I `2) where I is Element of R : I `1 = x  }
set X =  {  (I `2) where I is Element of R : I `1 = x  }  ;
thus  Im (R,x) c=  {  (I `2) where I is Element of R : I `1 = x  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (I `2) where I is Element of R : I `1 = x  }  c= Im (R,x)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Im (R,x) or z in  {  (I `2) where I is Element of R : I `1 = x  }  )
assume  z in Im (R,x) ; ::_thesis: z in  {  (I `2) where I is Element of R : I `1 = x  }
then consider y being set  such that
A1: [y,z] in R and
A2: y in {x} by RELAT_1:def_13;
A3: y = x by A2, TARSKI:def_1;
 ( y = [y,z] `1 & z = [y,z] `2 ) ;
hence  z in  {  (I `2) where I is Element of R : I `1 = x  }  by A1, A3; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (I `2) where I is Element of R : I `1 = x  }  or z in Im (R,x) )
assume  z in  {  (I `2) where I is Element of R : I `1 = x  }  ; ::_thesis: z in Im (R,x)
then consider I being Element of R such that
A4: z = I `2 and
A5: I `1 = x ;
A6: I = [(I `1),(I `2)] by Th21;
 x in {x} by TARSKI:def_1;
hence  z in Im (R,x) by A4, A5, A6, RELAT_1:def_13; ::_thesis: verum
end;

theorem :: MCART_1:88
for R being Relation
for x being set st x in R holds
x `2 in Im (R,(x `1))
proof
let R be Relation; ::_thesis: for x being set st x in R holds
x `2 in Im (R,(x `1))
let x be set ; ::_thesis: ( x in R implies x `2 in Im (R,(x `1)) )
assume A1: x in R ; ::_thesis: x `2 in Im (R,(x `1))
then  x `2 in  {  (I `2) where I is Element of R : I `1 = x `1  }  ;
hence  x `2 in Im (R,(x `1)) by A1, Th87; ::_thesis: verum
end;

theorem Th89: :: MCART_1:89
for y being set
for R being Relation
for x being set st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y
proof
let y be set ; ::_thesis: for R being Relation
for x being set st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y
let R be Relation; ::_thesis: for x being set st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y
let x be set ; ::_thesis: ( x in R & y in R & x `1 = y `1 & x `2 = y `2 implies x = y )
assume  ( x in R & y in R ) ; ::_thesis: ( not x `1 = y `1 or not x `2 = y `2 or x = y )
then  ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by Th21;
hence  ( not x `1 = y `1 or not x `2 = y `2 or x = y ) ; ::_thesis: verum
end;

theorem :: MCART_1:90
for R being non empty Relation
for x, y being Element of R st x `1 = y `1 & x `2 = y `2 holds
x = y by Th89;

theorem :: MCART_1:91
for x1, x2, x3, y1, y2, y3 being set holds proj1 (proj1 {[x1,x2,x3],[y1,y2,y3]}) = {x1,y1}
proof
let x1, x2, x3, y1, y2, y3 be set ; ::_thesis: proj1 (proj1 {[x1,x2,x3],[y1,y2,y3]}) = {x1,y1}
thus  proj1 (proj1 {[x1,x2,x3],[y1,y2,y3]}) = proj1 {[x1,x2],[y1,y2]} by RELAT_1:10
.= {x1,y1} by RELAT_1:10 ; ::_thesis: verum
end;

theorem :: MCART_1:92
for x1, x2, x3 being set holds proj1 (proj1 {[x1,x2,x3]}) = {x1}
proof
let x1, x2, x3 be set ; ::_thesis: proj1 (proj1 {[x1,x2,x3]}) = {x1}
thus  proj1 (proj1 {[x1,x2,x3]}) = proj1 {[x1,x2]} by RELAT_1:9
.= {x1} by RELAT_1:9 ; ::_thesis: verum
end;

scheme :: MCART_1:sch 1
BiFuncEx{ F1() ->  set , F2() ->  set , F3() ->  set , P1[ set , set , set ] } :
 ex f, g being Function st
( dom f = F1() & dom g = F1() & ( for x being set st x in F1() holds
P1[x,f . x,g . x] ) )
provided
A1: for x being set st x in F1() holds
ex y, z being set st
( y in F2() & z in F3() & P1[x,y,z] )
proof
defpred S1[ set , set ] means  for y, z being set st $2 `1 = y & $2 `2 = z holds
P1[$1,y,z];
A2: for x being set st x in F1() holds
ex p being set st
( p in [:F2(),F3():] & S1[x,p] )
proof
let x be set ; ::_thesis: ( x in F1() implies ex p being set st
( p in [:F2(),F3():] & S1[x,p] ) )
assume  x in F1() ; ::_thesis: ex p being set st
( p in [:F2(),F3():] & S1[x,p] )
then consider y, z being set  such that
A3: ( y in F2() & z in F3() ) and
A4: P1[x,y,z] by A1;
take p = [y,z]; ::_thesis: ( p in [:F2(),F3():] & S1[x,p] )
thus  p in [:F2(),F3():] by A3, ZFMISC_1:87; ::_thesis: S1[x,p]
thus  for y, z being set st p `1 = y & p `2 = z holds
P1[x,y,z] ::_thesis: verum
proof
let x1, x2 be set ; ::_thesis: ( p `1 = x1 & p `2 = x2 implies P1[x,x1,x2] )
assume that
A5: p `1 = x1 and
A6: p `2 = x2 ; ::_thesis: P1[x,x1,x2]
 x1 = y by A5, Th7;
hence  P1[x,x1,x2] by A4, A6, Th7; ::_thesis: verum
end;
end;
consider h being Function such that
 ( dom h = F1() & rng h c= [:F2(),F3():] ) and
A7: for x being set st x in F1() holds
S1[x,h . x] from FUNCT_1:sch_5(A2);
deffunc H1( set ) ->  set = (h . $1) `2 ;
deffunc H2( set ) ->  set = (h . $1) `1 ;
consider f being Function such that
A8: dom f = F1() and
A9: for x being set st x in F1() holds
f . x = H2(x) from FUNCT_1:sch_3();
consider g being Function such that
A10: dom g = F1() and
A11: for x being set st x in F1() holds
g . x = H1(x) from FUNCT_1:sch_3();
take  f ; ::_thesis: ex g being Function st
( dom f = F1() & dom g = F1() & ( for x being set st x in F1() holds
P1[x,f . x,g . x] ) )
take  g ; ::_thesis: ( dom f = F1() & dom g = F1() & ( for x being set st x in F1() holds
P1[x,f . x,g . x] ) )
thus  ( dom f = F1() & dom g = F1() ) by A8, A10; ::_thesis: for x being set st x in F1() holds
P1[x,f . x,g . x]
thus  for x being set st x in F1() holds
P1[x,f . x,g . x] ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in F1() implies P1[x,f . x,g . x] )
assume A12: x in F1() ; ::_thesis: P1[x,f . x,g . x]
then  ( f . x = (h . x) `1 & g . x = (h . x) `2 ) by A9, A11;
hence  P1[x,f . x,g . x] by A7, A12; ::_thesis: verum
end;
end;