:: MCART_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MCART_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th7: :: MCART_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set holds
( [x,y] `1 = x & [x,y] `2 = y ) by Def1, Def2;

theorem Th8: :: MCART_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, x, y being set st z in [:{x},{y}:] holds
( z `1 = x & z `2 = y )
proof end;

theorem :: MCART_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MCART_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: MCART_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X, Y being set st x in [:X,Y:] holds
x = [(x `1 ),(x `2 )]
proof end;

theorem Th24: :: MCART_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th28: :: MCART_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MCART_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[[x1,x2],x3],x4] ;

theorem :: MCART_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[x1,x2],x3,x4] ;

theorem Th33: :: MCART_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} )
proof end;

theorem Th36: :: MCART_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3 being set holds [:{x1},{x2},{x3}:] = {[x1,x2,x3]}
proof end;

theorem :: MCART_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, y1, x2, x3 being set holds [:{x1,y1},{x2},{x3}:] = {[x1,x2,x3],[y1,x2,x3]}
proof end;

theorem :: MCART_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, y2, x3 being set holds [:{x1},{x2,y2},{x3}:] = {[x1,x2,x3],[x1,y2,x3]}
proof end;

theorem :: MCART_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, y3 being set holds [:{x1},{x2},{x3,y3}:] = {[x1,x2,x3],[x1,x2,y3]}
proof end;

theorem :: MCART_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
proof end;

theorem Th54: :: MCART_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4 being set holds [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
proof end;

theorem Th55: :: MCART_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
proof end;

theorem Th56: :: MCART_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4 being set holds [:{x1},{x2},{x3},{x4}:] = {[x1,x2,x3,x4]}
proof end;

theorem Th66: :: MCART_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X, Y being set st x in [:X,Y:] holds
( x <> x `1 & x <> x `2 ) by Th66;

theorem :: MCART_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3 being set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X1, X2, X3, X4 being set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4
for 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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:119;
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 Th77;
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 Th88;
end;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;