:: Tuples, Projections and Cartesian Products
:: by Andrzej Trybulec
::
:: Received March 30, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


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 &amp; ( for x, y being set holds
( ( not x in X &amp; not y in X ) or not v = [x,y] ) ) )
proofend;

:: Now we prove theorems describing relationships between projections
:: of ordered pairs and Cartesian products of two sets.
theorem Th10: :: MCART_1:10
for z, X, Y being set st z in [:X,Y:] holds
( z `1 in X &amp; z `2 in Y )
proofend;

theorem :: MCART_1:11
for z, X, Y being set st ex x, y being set st z = [x,y] &amp; z `1 in X &amp; z `2 in Y holds
z in [:X,Y:]
proofend;

theorem :: MCART_1:12
for z, x, Y being set st z in [:{x},Y:] holds
( z `1 = x &amp; z `2 in Y )
proofend;

theorem :: MCART_1:13
for z, X, y being set st z in [:X,{y}:] holds
( z `1 in X &amp; z `2 = y )
proofend;

theorem :: MCART_1:14
for z, x, y being set st z in [:{x},{y}:] holds
( z `1 = x &amp; z `2 = y )
proofend;

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 ) &amp; z `2 in Y )
proofend;

theorem :: MCART_1:16
for z, X, y1, y2 being set st z in [:X,{y1,y2}:] holds
( z `1 in X &amp; ( z `2 = y1 or z `2 = y2 ) )
proofend;

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 ) &amp; z `2 = y )
proofend;

theorem :: MCART_1:18
for z, x, y1, y2 being set st z in [:{x},{y1,y2}:] holds
( z `1 = x &amp; ( z `2 = y1 or z `2 = y2 ) )
proofend;

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 ) &amp; ( z `2 = y1 or z `2 = y2 ) )
proofend;

theorem Th20: :: MCART_1:20
for x being set st ex y, z being set st x = [y,z] holds
( x <> x `1 &amp; x <> x `2 )
proofend;

theorem Th21: :: MCART_1:21
for x being set
for R being Relation st x in R holds
x = [(x `1),(x `2)]
proofend;

theorem :: MCART_1:22
for X, Y being set st X <> {} &amp; 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 <> {} &amp; 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]
proofend;

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]}
proofend;

theorem Th24: :: MCART_1:24
for X, Y being set st X <> {} &amp; Y <> {} holds
for x being Element of [:X,Y:] holds
( x <> x `1 &amp; x <> x `2 )
proofend;

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 &amp; ( for x, y, z being set holds
( ( not x in X &amp; not y in X ) or not v = [x,y,z] ) ) )
proofend;

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 &amp; ( for x1, x2, x3, x4 being set holds
( ( not x1 in X &amp; not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
proofend;

::
:: Cartesian products of three sets
::
theorem Th31: :: MCART_1:31
for X1, X2, X3 being set holds
( ( X1 <> {} &amp; X2 <> {} &amp; X3 <> {} ) iff [:X1,X2,X3:] <> {} )
proofend;

theorem Th32: :: MCART_1:32
for X1, X2, X3, Y1, Y2, Y3 being set st X1 <> {} &amp; X2 <> {} &amp; X3 <> {} &amp; [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds
( X1 = Y1 &amp; X2 = Y2 &amp; X3 = Y3 )
proofend;

theorem :: MCART_1:33
for X1, X2, X3, Y1, Y2, Y3 being set st [:X1,X2,X3:] <> {} &amp; [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds
( X1 = Y1 &amp; X2 = Y2 &amp; X3 = Y3 )
proofend;

theorem :: MCART_1:34
for X, Y being set st [:X,X,X:] = [:Y,Y,Y:] holds
X = Y
proofend;

Lm2:  for X1, X2, X3 being set st X1 <> {} &amp; X2 <> {} &amp; 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]
proofend;

theorem Th35: :: MCART_1:35
for x1, x2, x3 being set holds [:{x1},{x2},{x3}:] = {[x1,x2,x3]}
proofend;

theorem :: MCART_1:36
for x1, y1, x2, x3 being set holds [:{x1,y1},{x2},{x3}:] = {[x1,x2,x3],[y1,x2,x3]}
proofend;

theorem :: MCART_1:37
for x1, x2, y2, x3 being set holds [:{x1},{x2,y2},{x3}:] = {[x1,x2,x3],[x1,y2,x3]}
proofend;

theorem :: MCART_1:38
for x1, x2, x3, y3 being set holds [:{x1},{x2},{x3,y3}:] = {[x1,x2,x3],[x1,x2,y3]}
proofend;

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]}
proofend;

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]}
proofend;

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]}
proofend;

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]}
proofend;

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

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 &amp; x <> x `2_3 &amp; x <> x `3_3 )
proofend;

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 &amp; X2 meets Y2 &amp; X3 meets Y3 )
proofend;

::
:: Cartesian products of four sets
::
theorem Th49: :: MCART_1:49
for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
proofend;

theorem Th50: :: MCART_1:50
for X1, X2, X3, X4 being set holds [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
proofend;

theorem Th51: :: MCART_1:51
for X1, X2, X3, X4 being set holds
( ( X1 <> {} &amp; X2 <> {} &amp; X3 <> {} &amp; X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
proofend;

theorem Th52: :: MCART_1:52
for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st X1 <> {} &amp; X2 <> {} &amp; X3 <> {} &amp; X4 <> {} &amp; [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] holds
( X1 = Y1 &amp; X2 = Y2 &amp; X3 = Y3 &amp; X4 = Y4 )
proofend;

theorem :: MCART_1:53
for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st [:X1,X2,X3,X4:] <> {} &amp; [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] holds
( X1 = Y1 &amp; X2 = Y2 &amp; X3 = Y3 &amp; X4 = Y4 )
proofend;

theorem :: MCART_1:54
for X, Y being set st [:X,X,X,X:] = [:Y,Y,Y,Y:] holds
X = Y
proofend;

Lm3:  for X1, X2, X3, X4 being set st X1 <> {} &amp; X2 <> {} &amp; X3 <> {} &amp; 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]
proofend;

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
proofend;
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
proofend;
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 )
proofend;
:: 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
proofend;
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 )
proofend;
:: 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
proofend;
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 )
proofend;
:: 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
proofend;
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 )
proofend;
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 &amp; x <> x `2_4 &amp; x <> x `3_4 &amp; x <> x `4_4 )
proofend;

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

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 &amp; X2 meets Y2 &amp; X3 meets Y3 &amp; X4 meets Y4 )
proofend;

theorem :: MCART_1:61
for x1, x2, x3, x4 being set holds [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
proofend;

:: Ordered pairs
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 &amp; x <> x `2 )
proofend;

theorem :: MCART_1:63
for x, X, Y being set st x in [:X,Y:] holds
( x <> x `1 &amp; 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 &amp; x `2_3 = x2 &amp; 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
proofend;

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

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

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 &amp; x2 in X2 &amp; x3 in X3 &amp; z = [x1,x2,x3] )
proofend;

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 &amp; x2 in X2 &amp; x3 in X3 ) )
proofend;

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 &amp; x2 in X2 &amp; x3 in X3 &amp; z = [x1,x2,x3] ) ) ) holds
Z = [:X1,X2,X3:]
proofend;

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 &amp; x `2_3 in A2 &amp; x `3_3 in A3 )
proofend;

theorem Th73: :: MCART_1:73
for X1, Y1, X2, Y2, X3, Y3 being set st X1 c= Y1 &amp; X2 c= Y2 &amp; X3 c= Y3 holds
[:X1,X2,X3:] c= [:Y1,Y2,Y3:]
proofend;

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 &amp; x `2_4 = x2 &amp; x `3_4 = x3 &amp; 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
proofend;

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

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

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

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 &amp; x2 in X2 &amp; x3 in X3 &amp; x4 in X4 &amp; z = [x1,x2,x3,x4] )
proofend;

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 &amp; x2 in X2 &amp; x3 in X3 &amp; x4 in X4 ) )
proofend;

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 &amp; x2 in X2 &amp; x3 in X3 &amp; x4 in X4 &amp; z = [x1,x2,x3,x4] ) ) ) holds
Z = [:X1,X2,X3,X4:]
proofend;

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 &amp; x `2_4 in A2 &amp; x `3_4 in A3 &amp; x `4_4 in A4 )
proofend;

theorem Th84: :: MCART_1:84
for X1, Y1, X2, Y2, X3, Y3, X4, Y4 being set st X1 c= Y1 &amp; X2 c= Y2 &amp; X3 c= Y3 &amp; X4 c= Y4 holds
[:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]
proofend;

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

:: from DTCONSTR
definition
let f be Function;
func pr1 f ->  Function means :: MCART_1:def 12
( dom it = dom f &amp; ( 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 &amp; ( for x being set st x in dom f holds
b1 . x = (f . x) `1 ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom f holds
b1 . x = (f . x) `1 ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom f holds
b2 . x = (f . x) `1 ) holds
b1 = b2
proofend;
func pr2 f ->  Function means :: MCART_1:def 13
( dom it = dom f &amp; ( 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 &amp; ( for x being set st x in dom f holds
b1 . x = (f . x) `2 ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom f holds
b1 . x = (f . x) `2 ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom f holds
b2 . x = (f . x) `2 ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines pr1 MCART_1:def_12_:_
 for f, b2 being Function holds
( b2 = pr1 f iff ( dom b2 = dom f &amp; ( 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 &amp; ( 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 &amp; [[x1,x2],y] `12 = x2 &amp; [x,[y1,y2]] `21 = y1 &amp; [x,[y1,y2]] `22 = y2 ) ;

:: missing, 2007.04.13, A.T.
theorem :: MCART_1:86
for R being Relation
for x being set st x in R holds
( x `1 in dom R &amp; x `2 in rng R )
proofend;

:: 2009.08.29, A.T.
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  }
proofend;

theorem :: MCART_1:88
for R being Relation
for x being set st x in R holds
x `2 in Im (R,(x `1))
proofend;

theorem Th89: :: MCART_1:89
for y being set
for R being Relation
for x being set st x in R &amp; y in R &amp; x `1 = y `1 &amp; x `2 = y `2 holds
x = y
proofend;

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

:: 2010.05.120, A.T.
theorem :: MCART_1:91
for x1, x2, x3, y1, y2, y3 being set holds proj1 (proj1 {[x1,x2,x3],[y1,y2,y3]}) = {x1,y1}
proofend;

theorem :: MCART_1:92
for x1, x2, x3 being set holds proj1 (proj1 {[x1,x2,x3]}) = {x1}
proofend;

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() &amp; dom g = F1() &amp; ( 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() &amp; z in F3() &amp; P1[x,y,z] )
proofend;