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


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

theorem :: MCART_1:8
canceled;

::
:: Ordered pairs
::
:: Now we introduce the projections of ordered pairs (functions that assign
:: to an ordered pair its first and its second element). The definitions
:: are permissive, function are defined for an arbitrary object. If it is not
:: an ordered pair, they are of course meaningless.
::$CT 8
theorem :: MCART_1:9
for X being set st X <> {} holds
ex v being object st
( v in X & ( for x, y being object holds
( ( not x in X & not y in X ) or not v = [x,y] ) ) )
proof end;

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

theorem :: MCART_1:11
canceled;

::$CT
theorem :: MCART_1:12
for x, z being object
for Y being set st z in [:{x},Y:] holds
( z `1 = x & z `2 in Y )
proof end;

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

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

theorem :: MCART_1:15
for x1, x2, z being object
for 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 y1, y2, z being object
for X 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 x1, x2, y, z being object st z in [:{x1,x2},{y}:] holds
( ( z `1 = x1 or z `1 = x2 ) & z `2 = y )
proof end;

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

theorem :: MCART_1:19
for x1, x2, y1, y2, z being object 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 Th14: :: MCART_1:20
for x being object st ex y, z being object st x = [y,z] holds
( x <> x `1 & x <> x `2 )
proof end;

theorem Th15: :: MCART_1:21
for x being object
for R being Relation st x in R 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;

registration
let X1, X2 be non empty set ;
cluster -> pair for Element of [:X1,X2:];
coherence
for b1 being Element of [:X1,X2:] holds b1 is pair
proof end;
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 Th15;

theorem Th17: :: MCART_1:23
for x1, x2, y1, y2 being object holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof end;

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

theorem :: MCART_1:25
canceled;

::
:: Triples
::
::$CT
theorem Th19: :: MCART_1:26
for X being set st X <> {} holds
ex v being object st
( v in X & ( for x, y, z being object holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )
proof end;

theorem :: MCART_1:27
canceled;

theorem :: MCART_1:28
canceled;

theorem :: MCART_1:29
canceled;

::
:: Quadruples
::
::$CT 3
theorem Th20: :: MCART_1:30
for X being set st X <> {} holds
ex v being object st
( v in X & ( for x1, x2, x3, x4 being object holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
proof end;

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

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

theorem :: MCART_1:34
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 Th25: :: MCART_1:35
for x1, x2, x3 being object holds [:{x1},{x2},{x3}:] = {[x1,x2,x3]}
proof end;

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

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

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

theorem :: MCART_1:39
for x1, x2, x3, y1, y2 being object holds [:{x1,y1},{x2,y2},{x3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3]}
proof end;

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

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

theorem :: MCART_1:42
for x1, x2, x3, y1, y2, y3 being object 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;

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

definition
let X1, X2, X3 be non empty set ;
let x be Element of [:X1,X2,X3:];
:: original: `1_3
redefine func x `1_3 -> Element of X1 means :: MCART_1:def 5
 for x1, x2, x3 being object st x = [x1,x2,x3] holds
it = x1;
coherence
x `1_3 is Element of X1
proof end;
compatibility
for b1 being Element of X1 holds
( b1 = x `1_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds
b1 = x1 )
proof end;
:: original: `2_3
redefine func x `2_3 -> Element of X2 means :: MCART_1:def 6
 for x1, x2, x3 being object st x = [x1,x2,x3] holds
it = x2;
coherence
x `2_3 is Element of X2
proof end;
compatibility
for b1 being Element of X2 holds
( b1 = x `2_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds
b1 = x2 )
proof end;
:: original: `2
redefine func x `3_3 -> Element of X3 means :: MCART_1:def 7
 for x1, x2, x3 being object st x = [x1,x2,x3] holds
it = x3;
coherence
x `2 is Element of X3
proof end;
compatibility
for b1 being Element of X3 holds
( b1 = x `2 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds
b1 = x3 )
proof 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 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 object st x = [x1,x2,x3] holds
b5 = x1 );

:: deftheorem 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 object st x = [x1,x2,x3] holds
b5 = x2 );

:: deftheorem 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 object st x = [x1,x2,x3] holds
b5 = x3 );

theorem :: MCART_1:43
canceled;

theorem :: MCART_1:44
canceled;

::$CT 2
theorem Th34: :: 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 end;

theorem :: MCART_1:46
canceled;

::$CT
theorem Th35: :: 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 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 end;

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

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

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

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

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

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 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 func x `1_4 -> Element of X1 means :: MCART_1:def 8
 for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
it = x1;
coherence
x `1_4 is Element of X1
proof end;
compatibility
for b1 being Element of X1 holds
( b1 = x `1_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
b1 = x1 )
proof end;
:: original: `2_4
redefine func x `2_4 -> Element of X2 means :: MCART_1:def 9
 for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
it = x2;
coherence
x `2_4 is Element of X2
proof end;
compatibility
for b1 being Element of X2 holds
( b1 = x `2_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
b1 = x2 )
proof end;
:: original: `2_3
redefine func x `3_4 -> Element of X3 means :: MCART_1:def 10
 for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
it = x3;
coherence
x `2_3 is Element of X3
proof end;
compatibility
for b1 being Element of X3 holds
( b1 = x `2_3 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
b1 = x3 )
proof end;
:: original: `2
redefine func x `4_4 -> Element of X4 means :: MCART_1:def 11
 for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
it = x4;
coherence
x `2 is Element of X4
proof end;
compatibility
for b1 being Element of X4 holds
( b1 = x `2 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
b1 = x4 )
proof end;
end;

:: deftheorem 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 object st x = [x1,x2,x3,x4] holds
b6 = x1 );

:: deftheorem 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 object st x = [x1,x2,x3,x4] holds
b6 = x2 );

:: deftheorem 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 object st x = [x1,x2,x3,x4] holds
b6 = x3 );

:: deftheorem 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 object st x = [x1,x2,x3,x4] holds
b6 = x4 );

theorem :: MCART_1:55
canceled;

theorem :: MCART_1:56
canceled;

theorem :: MCART_1:57
canceled;

::$CT 3
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 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 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 end;

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

:: Ordered pairs
theorem Th48: :: 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 end;

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

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 object st x = [x1,x2,x3] holds
( x `1_3 = x1 & x `2_3 = x2 & x `3_3 = x3 ) ;

theorem :: MCART_1:65
for y1 being object
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 end;

theorem :: MCART_1:66
for y2 being object
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 end;

theorem :: MCART_1:67
for y3 being object
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 end;

theorem Th54: :: MCART_1:68
for z being object
for X1, X2, X3 being set st z in [:X1,X2,X3:] holds
ex x1, x2, x3 being object st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] )
proof end;

theorem Th55: :: MCART_1:69
for x1, x2, x3 being object
for 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:70
for X1, X2, X3, Z being set st ( for z being object holds
( z in Z iff ex x1, x2, x3 being object st
( x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3] ) ) ) holds
Z = [:X1,X2,X3:]
proof end;

theorem :: MCART_1:71
canceled;

::$CT
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 end;

theorem Th58: :: MCART_1:73
for X1, X2, X3, Y1, Y2, 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: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 ) ;

theorem :: MCART_1:75
for y1 being object
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 end;

theorem :: MCART_1:76
for y2 being object
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 end;

theorem :: MCART_1:77
for y3 being object
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 end;

theorem :: MCART_1:78
for y4 being object
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 end;

theorem :: MCART_1:79
for z being object
for X1, X2, X3, X4 being set st z in [:X1,X2,X3,X4:] holds
ex x1, x2, x3, x4 being object st
( x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4] )
proof end;

theorem :: MCART_1:80
for x1, x2, x3, x4 being object
for 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:81
for X1, X2, X3, X4, Z being set st ( for z being object holds
( z in Z iff ex x1, x2, x3, x4 being object 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 :: MCART_1:82
canceled;

::$CT
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 end;

theorem Th68: :: MCART_1:84
for X1, X2, X3, X4, Y1, Y2, Y3, 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 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 Th58;
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 Th68;
end;

:: from DTCONSTR
definition
let f be Function;
func pr1 f -> Function means :: MCART_1:def 12
( dom it = dom f & ( for x being object st x in dom f holds
it . x = (f . x) `1 ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object 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 object st x in dom f holds
b1 . x = (f . x) `1 ) & dom b2 = dom f & ( for x being object 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 object st x in dom f holds
it . x = (f . x) `2 ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object 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 object st x in dom f holds
b1 . x = (f . x) `2 ) & dom b2 = dom f & ( for x being object 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 object 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 object st x in dom f holds
b2 . x = (f . x) `2 ) ) );

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

:: deftheorem defines `11 MCART_1:def 14 :
for x being object holds x `11 = (x `1) `1 ;

:: deftheorem defines `12 MCART_1:def 15 :
for x being object holds x `12 = (x `1) `2 ;

:: deftheorem defines `21 MCART_1:def 16 :
for x being object holds x `21 = (x `2) `1 ;

:: deftheorem defines `22 MCART_1:def 17 :
for x being object holds x `22 = (x `2) `2 ;

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

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

:: 2009.08.29, A.T.
theorem Th71: :: MCART_1:87
for R being non empty Relation
for x being object holds Im (R,x) = { (I `2) where I is Element of R : I `1 = x }
proof end;

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

theorem Th73: :: MCART_1:89
for y being object
for R being Relation
for x being object st x in R & y in R & x `1 = y `1 & x `2 = y `2 holds
x = y
proof 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 Th73;

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

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

scheme :: MCART_1:sch 1
BiFuncEx{ F1() -> set , F2() -> set , F3() -> set , P1[ object , object , object ] } :
ex f, g being Function st
( dom f = F1() & dom g = F1() & ( for x being object st x in F1() holds
P1[x,f . x,g . x] ) )
provided
A1: for x being object st x in F1() holds
ex y, z being object st
( y in F2() & z in F3() & P1[x,y,z] )
proof end;

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