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


begin

theorem Th1: :: MCART_1:1
for X being set st X <> {} holds
ex Y being set st
( Y in X & Y misses X )
proof end;

theorem Th2: :: MCART_1:2
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1 being set st Y1 in Y holds
Y1 misses X ) )
proof end;

theorem :: MCART_1:3
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2 being set st Y1 in Y2 & Y2 in Y holds
Y1 misses X ) )
proof end;

theorem Th4: :: MCART_1:4
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds
Y1 misses X ) )
proof end;

theorem :: MCART_1:5
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y holds
Y1 misses X ) )
proof end;

theorem Th6: :: MCART_1:6
for X being set st X <> {} holds
ex Y being set st
( Y in X & ( 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 ) )
proof end;

definition
let x be set ;
given x1, x2 being set such that A1: x = [x1,x2] ;
func x `1 -> set means :Def1: :: MCART_1:def 1
for y1, y2 being set st x = [y1,y2] holds
it = y1;
existence
ex b1 being set st
for y1, y2 being set st x = [y1,y2] holds
b1 = y1
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2 being set st x = [y1,y2] holds
b1 = y1 ) & ( for y1, y2 being set st x = [y1,y2] holds
b2 = y1 ) holds
b1 = b2
proof end;
func x `2 -> set means :Def2: :: MCART_1:def 2
for y1, y2 being set st x = [y1,y2] holds
it = y2;
existence
ex b1 being set st
for y1, y2 being set st x = [y1,y2] holds
b1 = y2
proof end;
uniqueness
for b1, b2 being set st ( for y1, y2 being set st x = [y1,y2] holds
b1 = y2 ) & ( for y1, y2 being set st x = [y1,y2] holds
b2 = y2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines `1 MCART_1:def 1 :
for x being set st ex x1, x2 being set st x = [x1,x2] holds
for b2 being set holds
( b2 = x `1 iff for y1, y2 being set st x = [y1,y2] holds
b2 = y1 );

:: deftheorem Def2 defines `2 MCART_1:def 2 :
for x being set st ex x1, x2 being set st x = [x1,x2] holds
for b2 being set holds
( b2 = x `2 iff for y1, y2 being set st x = [y1,y2] holds
b2 = y2 );

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

theorem Th8: :: MCART_1:8
for z being set st ex x, y being set st z = [x,y] holds
[(z `1 ),(z `2 )] = z
proof end;

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

theorem :: MCART_1:14
for z, x, y being set st z in [:{x},{y}:] holds
( z `1 = x & z `2 = y )
proof 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 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 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 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 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 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 end;

theorem :: MCART_1:21
canceled;

theorem :: MCART_1:22
canceled;

theorem Th23: :: MCART_1:23
for x being set
for R being Relation st x in R holds
x = [(x `1 ),(x `2 )]
proof 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 `2 )]
proof end;

Lm1: for X1, X2 being set st X1 <> {} & X2 <> {} holds
for x being Element of [:X1,X2:] ex xx1 being Element of X1 ex xx2 being Element of X2 st x = [xx1,xx2]
proof end;

theorem Th25: :: MCART_1:25
for x1, x2, y1, y2 being set holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof end;

theorem Th26: :: MCART_1:26
for X, Y being set st X <> {} & Y <> {} holds
for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
proof end;

definition
let x1, x2, x3 be set ;
func [x1,x2,x3] -> set equals :: MCART_1:def 3
[[x1,x2],x3];
coherence
[[x1,x2],x3] is set ;
end;

:: deftheorem defines [ MCART_1:def 3 :
for x1, x2, x3 being set holds [x1,x2,x3] = [[x1,x2],x3];

theorem :: MCART_1:27
canceled;

theorem Th28: :: MCART_1:28
for x1, x2, x3, y1, y2, y3 being set st [x1,x2,x3] = [y1,y2,y3] holds
( x1 = y1 & x2 = y2 & x3 = y3 )
proof end;

theorem Th29: :: MCART_1:29
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 end;

definition
let x1, x2, x3, x4 be set ;
func [x1,x2,x3,x4] -> set equals :: MCART_1:def 4
[[x1,x2,x3],x4];
coherence
[[x1,x2,x3],x4] is set ;
end;

:: deftheorem defines [ MCART_1:def 4 :
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[x1,x2,x3],x4];

theorem :: MCART_1:30
canceled;

theorem :: MCART_1:31
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[[x1,x2],x3],x4] ;

theorem :: MCART_1:32
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[x1,x2],x3,x4] ;

theorem Th33: :: MCART_1:33
for x1, x2, x3, x4, y1, y2, y3, y4 being set st [x1,x2,x3,x4] = [y1,y2,y3,y4] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
proof end;

theorem Th34: :: MCART_1:34
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 end;

theorem Th35: :: MCART_1:35
for X1, X2, X3 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} )
proof end;

theorem Th36: :: MCART_1:36
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 end;

theorem :: MCART_1:37
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 end;

theorem :: MCART_1:38
for X, Y being set st [:X,X,X:] = [:Y,Y,Y:] holds
X = Y
proof end;

Lm2: for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 st x = [xx1,xx2,xx3]
proof end;

theorem Th39: :: MCART_1:39
for x1, x2, x3 being set holds [:{x1},{x2},{x3}:] = {[x1,x2,x3]}
proof end;

theorem :: MCART_1:40
for x1, y1, x2, x3 being set holds [:{x1,y1},{x2},{x3}:] = {[x1,x2,x3],[y1,x2,x3]}
proof end;

theorem :: MCART_1:41
for x1, x2, y2, x3 being set holds [:{x1},{x2,y2},{x3}:] = {[x1,x2,x3],[x1,y2,x3]}
proof end;

theorem :: MCART_1:42
for x1, x2, x3, y3 being set holds [:{x1},{x2},{x3,y3}:] = {[x1,x2,x3],[x1,x2,y3]}
proof end;

theorem :: MCART_1:43
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 end;

theorem :: MCART_1:44
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 end;

theorem :: MCART_1:45
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 end;

theorem :: MCART_1:46
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 end;

definition
let X1, X2, X3 be set ;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} ) ;
let x be Element of [:X1,X2,X3:];
func x `1 -> Element of X1 means :Def5: :: MCART_1:def 5
for x1, x2, x3 being set st x = [x1,x2,x3] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x1
proof end;
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x1 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> Element of X2 means :Def6: :: MCART_1:def 6
for x1, x2, x3 being set st x = [x1,x2,x3] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x2
proof end;
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x2 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> Element of X3 means :Def7: :: MCART_1:def 7
for x1, x2, x3 being set st x = [x1,x2,x3] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x3
proof end;
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
b1 = x3 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
b2 = x3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines `1 MCART_1:def 5 :
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:]
for b5 being Element of X1 holds
( b5 = x `1 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b5 = x1 );

:: deftheorem Def6 defines `2 MCART_1:def 6 :
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:]
for b5 being Element of X2 holds
( b5 = x `2 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b5 = x2 );

:: deftheorem Def7 defines `3 MCART_1:def 7 :
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:]
for b5 being Element of X3 holds
( b5 = x `3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
b5 = x3 );

theorem :: MCART_1:47
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:]
for x1, x2, x3 being set st x = [x1,x2,x3] holds
( x `1 = x1 & x `2 = x2 & x `3 = x3 ) by Def5, Def6, Def7;

theorem Th48: :: MCART_1:48
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:] holds x = [(x `1 ),(x `2 ),(x `3 )]
proof end;

theorem Th49: :: MCART_1:49
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 end;

theorem Th50: :: MCART_1:50
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:] holds
( x `1 = (x `1 ) `1 & x `2 = (x `1 ) `2 & x `3 = x `2 )
proof end;

theorem Th51: :: MCART_1:51
for X1, X2, X3 being set st X1 <> {} & X2 <> {} & X3 <> {} holds
for x being Element of [:X1,X2,X3:] holds
( x <> x `1 & x <> x `2 & x <> x `3 )
proof end;

theorem :: MCART_1:52
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 end;

theorem Th53: :: MCART_1:53
for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
proof end;

theorem Th54: :: MCART_1:54
for X1, X2, X3, X4 being set holds [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
proof end;

theorem Th55: :: MCART_1:55
for X1, X2, X3, X4 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
proof end;

theorem Th56: :: MCART_1:56
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 end;

theorem :: MCART_1:57
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 end;

theorem :: MCART_1:58
for X, Y being set st [:X,X,X,X:] = [:Y,Y,Y,Y:] holds
X = Y
proof end;

Lm3: for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:] ex xx1 being Element of X1 ex xx2 being Element of X2 ex xx3 being Element of X3 ex xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4]
proof end;

definition
let X1, X2, X3, X4 be set ;
assume A1: ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) ;
let x be Element of [:X1,X2,X3,X4:];
func x `1 -> 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;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x1
proof end;
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x1 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b2 = x1 ) holds
b1 = b2
proof end;
func x `2 -> 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;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x2
proof end;
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x2 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b2 = x2 ) holds
b1 = b2
proof end;
func x `3 -> 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;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x3
proof end;
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x3 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b2 = x3 ) holds
b1 = b2
proof end;
func x `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;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x4
proof end;
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b1 = x4 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b2 = x4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines `1 MCART_1:def 8 :
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X1 holds
( b6 = x `1 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x1 );

:: deftheorem Def9 defines `2 MCART_1:def 9 :
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X2 holds
( b6 = x `2 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x2 );

:: deftheorem Def10 defines `3 MCART_1:def 10 :
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X3 holds
( b6 = x `3 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x3 );

:: deftheorem Def11 defines `4 MCART_1:def 11 :
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:]
for b6 being Element of X4 holds
( b6 = x `4 iff for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
b6 = x4 );

theorem :: MCART_1:59
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
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 = x1 & x `2 = x2 & x `3 = x3 & x `4 = x4 ) by Def8, Def9, Def10, Def11;

theorem Th60: :: MCART_1:60
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:] holds x = [(x `1 ),(x `2 ),(x `3 ),(x `4 )]
proof end;

theorem Th61: :: MCART_1:61
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:] holds
( x `1 = ((x `1 ) `1 ) `1 & x `2 = ((x `1 ) `1 ) `2 & x `3 = (x `1 ) `2 & x `4 = x `2 )
proof end;

theorem :: MCART_1:62
for X1, X2, X3, X4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} holds
for x being Element of [:X1,X2,X3,X4:] holds
( x <> x `1 & x <> x `2 & x <> x `3 & x <> x `4 )
proof end;

theorem :: MCART_1:63
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 end;

theorem :: MCART_1:64
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 end;

theorem :: MCART_1:65
for x1, x2, x3, x4 being set holds [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
proof end;

theorem Th66: :: MCART_1:66
for X, Y being set st [:X,Y:] <> {} holds
for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )
proof end;

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

theorem :: MCART_1:68
for X1, X2, X3 being set
for x being Element of [:X1,X2,X3:] st X1 <> {} & X2 <> {} & X3 <> {} holds
for x1, x2, x3 being set st x = [x1,x2,x3] holds
( x `1 = x1 & x `2 = x2 & x `3 = x3 ) by Def5, Def6, Def7;

theorem :: MCART_1:69
for X1, X2, X3, y1 being set
for x being Element of [:X1,X2,X3:] st X1 <> {} & X2 <> {} & X3 <> {} & ( 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
proof end;

theorem :: MCART_1:70
for X1, X2, X3, y2 being set
for x being Element of [:X1,X2,X3:] st X1 <> {} & X2 <> {} & X3 <> {} & ( 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
proof end;

theorem :: MCART_1:71
for X1, X2, X3, y3 being set
for x being Element of [:X1,X2,X3:] st X1 <> {} & X2 <> {} & X3 <> {} & ( 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
proof end;

theorem Th72: :: MCART_1:72
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 end;

theorem Th73: :: MCART_1:73
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 end;

theorem :: MCART_1:74
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 end;

theorem Th75: :: MCART_1:75
for X1, X2, X3, Y1, Y2, Y3 being set st X1 <> {} & X2 <> {} & X3 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} holds
for x being Element of [:X1,X2,X3:]
for y being Element of [:Y1,Y2,Y3:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 )
proof end;

theorem :: MCART_1:76
for X1, X2, X3 being set
for A1 being Subset of
for A2 being Subset of
for A3 being Subset of
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 )
proof end;

theorem Th77: :: MCART_1:77
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 end;

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

theorem :: MCART_1:79
for X1, X2, X3, X4, y1 being set
for x being Element of [:X1,X2,X3,X4:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & ( 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
proof end;

theorem :: MCART_1:80
for X1, X2, X3, X4, y2 being set
for x being Element of [:X1,X2,X3,X4:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & ( 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
proof end;

theorem :: MCART_1:81
for X1, X2, X3, X4, y3 being set
for x being Element of [:X1,X2,X3,X4:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & ( 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
proof end;

theorem :: MCART_1:82
for X1, X2, X3, X4, y4 being set
for x being Element of [:X1,X2,X3,X4:] st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & ( 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
proof end;

theorem :: MCART_1:83
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 end;

theorem :: MCART_1:84
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 end;

theorem :: MCART_1:85
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 end;

theorem Th86: :: MCART_1:86
for X1, X2, X3, X4, Y1, Y2, Y3, Y4 being set st X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} & Y4 <> {} holds
for x being Element of [:X1,X2,X3,X4:]
for y being Element of [:Y1,Y2,Y3,Y4:] st x = y holds
( x `1 = y `1 & x `2 = y `2 & x `3 = y `3 & x `4 = y `4 )
proof end;

theorem :: MCART_1:87
for X1, X2, X3, X4 being set
for A1 being Subset of
for A2 being Subset of
for A3 being Subset of
for A4 being Subset of
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds
( x `1 in A1 & x `2 in A2 & x `3 in A3 & x `4 in A4 )
proof end;

theorem Th88: :: MCART_1:88
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 end;

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

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

definition
let X1, X2, X3, X4 be set ;
let A1 be Subset of ;
let A2 be Subset of ;
let A3 be Subset of ;
let A4 be Subset of ;
:: original: [:
redefine func [:A1,A2,A3,A4:] -> Subset of ;
coherence
[:A1,A2,A3,A4:] is Subset of by Th88;
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 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 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 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 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 ;
func x `11 -> set equals :: MCART_1:def 14
(x `1 ) `1 ;
coherence
(x `1 ) `1 is set ;
func x `12 -> set equals :: MCART_1:def 15
(x `1 ) `2 ;
coherence
(x `1 ) `2 is set ;
func x `21 -> set equals :: MCART_1:def 16
(x `2 ) `1 ;
coherence
(x `2 ) `1 is set ;
func x `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:89
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 )
proof end;

theorem :: MCART_1:90
canceled;

theorem :: MCART_1:91
for R being Relation
for x being set st x in R holds
( x `1 in dom R & x `2 in rng R )
proof end;

theorem Th92: :: MCART_1:92
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 end;

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

theorem Th94: :: MCART_1:94
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 end;

theorem :: MCART_1:95
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 Th94;