:: by Andrzej Trybulec

::

:: Received March 30, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem Th1: :: MCART_1:1

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 b_{1} being set st

for y1, y2 being set st x = [y1,y2] holds

b_{1} = y1

for b_{1}, b_{2} being set st ( for y1, y2 being set st x = [y1,y2] holds

b_{1} = y1 ) & ( for y1, y2 being set st x = [y1,y2] holds

b_{2} = y1 ) holds

b_{1} = b_{2}

for y1, y2 being set st x = [y1,y2] holds

it = y2;

existence

ex b_{1} being set st

for y1, y2 being set st x = [y1,y2] holds

b_{1} = y2

for b_{1}, b_{2} being set st ( for y1, y2 being set st x = [y1,y2] holds

b_{1} = y2 ) & ( for y1, y2 being set st x = [y1,y2] holds

b_{2} = y2 ) holds

b_{1} = b_{2}

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

for y1, y2 being set st x = [y1,y2] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> set means :Def2: :: MCART_1:def 2for y1, y2 being set st x = [y1,y2] holds

it = y2;

existence

ex b

for y1, y2 being set st x = [y1,y2] holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b

( b

b

:: deftheorem Def2 defines `2 MCART_1:def 2 :

for x being set st ex x1, x2 being set st x = [x1,x2] holds

for b

( b

b

theorem :: MCART_1:7

theorem Th8: :: MCART_1:8

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] ) ) )

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

proof end;

theorem :: MCART_1:11

proof end;

theorem :: MCART_1:12

proof end;

theorem :: MCART_1:13

proof end;

theorem :: MCART_1:14

proof end;

theorem :: MCART_1:15

proof end;

theorem :: MCART_1:16

proof end;

theorem :: MCART_1:17

proof end;

theorem :: MCART_1:18

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 ) )

( ( z `1 = x1 or z `1 = x2 ) & ( z `2 = y1 or z `2 = y2 ) )

proof end;

theorem Th20: :: MCART_1:20

proof end;

theorem :: MCART_1:21

canceled;

theorem :: MCART_1:22

canceled;

theorem Th23: :: MCART_1:23

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)]

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

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 )

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;
func [x1,x2,x3] -> set equals :: MCART_1:def 3

[[x1,x2],x3];

coherence

[[x1,x2],x3] is set ;

:: 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 )

( 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] ) ) )

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;
func [x1,x2,x3,x4] -> set equals :: MCART_1:def 4

[[x1,x2,x3],x4];

coherence

[[x1,x2,x3],x4] is set ;

:: 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

theorem :: MCART_1:32

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 )

( 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] ) ) )

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

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 )

( 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 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 )

proof end;

theorem :: MCART_1:38

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

proof end;

theorem :: MCART_1:40

proof end;

theorem :: MCART_1:41

proof end;

theorem :: MCART_1:42

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 b_{1} being Element of X1 st

for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{1} = x1 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3 being set st x = [x1,x2,x3] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{1} = x2 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3 being set st x = [x1,x2,x3] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{1} = x3 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

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

for x1, x2, x3 being set st x = [x1,x2,x3] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def6: :: MCART_1:def 6for x1, x2, x3 being set st x = [x1,x2,x3] holds

it = x2;

existence

ex b

for x1, x2, x3 being set st x = [x1,x2,x3] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def7: :: MCART_1:def 7for x1, x2, x3 being set st x = [x1,x2,x3] holds

it = x3;

existence

ex b

for x1, x2, x3 being set st x = [x1,x2,x3] holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b

( b

b

:: 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 b

( b

b

:: 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 b

( b

b

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;

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)]

for x being Element of [:X1,X2,X3:] holds x = [(x `1),(x `2),(x `3)]

proof end;

theorem Th49: :: MCART_1:49

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 )

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 )

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 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 )

proof end;

theorem Th53: :: MCART_1:53

proof end;

theorem Th54: :: MCART_1:54

proof end;

theorem Th55: :: MCART_1:55

for X1, X2, X3, X4 being set holds

( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )

( ( 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 )

( 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 )

( X1 = Y1 & X2 = Y2 & X3 = Y3 & X4 = Y4 )

proof end;

theorem :: MCART_1:58

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 b_{1} being Element of X1 st

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x1

for b_{1}, b_{2} being Element of X1 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x1 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{2} = x1 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

it = x2;

existence

ex b_{1} being Element of X2 st

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x2

for b_{1}, b_{2} being Element of X2 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x2 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{2} = x2 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

it = x3;

existence

ex b_{1} being Element of X3 st

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x3

for b_{1}, b_{2} being Element of X3 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x3 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{2} = x3 ) holds

b_{1} = b_{2}

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

it = x4;

existence

ex b_{1} being Element of X4 st

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x4

for b_{1}, b_{2} being Element of X4 st ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{1} = x4 ) & ( for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b_{2} = x4 ) holds

b_{1} = b_{2}

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

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `2 -> Element of X2 means :Def9: :: MCART_1:def 9for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

it = x2;

existence

ex b

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `3 -> Element of X3 means :Def10: :: MCART_1:def 10for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

it = x3;

existence

ex b

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func x `4 -> Element of X4 means :Def11: :: MCART_1:def 11for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

it = x4;

existence

ex b

for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b

( b

b

:: 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 b

( b

b

:: 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 b

( b

b

:: 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 b

( b

b

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;

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)]

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 )

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 )

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

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 )

( X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 )

proof end;

theorem :: MCART_1:65

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 )

for x being Element of [:X,Y:] holds

( x <> x `1 & x <> x `2 )

proof end;

theorem :: MCART_1:67

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;

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

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

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

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] )

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 ) )

( [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:]

( 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 )

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 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 )

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

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:]

[: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;

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

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

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

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

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] )

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 ) )

( [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:]

( 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 )

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 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 )

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

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:]

[: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;
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;

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

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

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 b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom f holds

b_{1} . x = (f . x) `1 ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom f holds

b_{1} . x = (f . x) `1 ) & dom b_{2} = dom f & ( for x being set st x in dom f holds

b_{2} . x = (f . x) `1 ) holds

b_{1} = b_{2}

( dom it = dom f & ( for x being set st x in dom f holds

it . x = (f . x) `2 ) );

existence

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom f holds

b_{1} . x = (f . x) `2 ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom f holds

b_{1} . x = (f . x) `2 ) & dom b_{2} = dom f & ( for x being set st x in dom f holds

b_{2} . x = (f . x) `2 ) holds

b_{1} = b_{2}

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

( dom b

b

proof end;

uniqueness for b

b

b

b

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 b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines pr1 MCART_1:def 12 :

for f, b

( b

b

:: deftheorem defines pr2 MCART_1:def 13 :

for f, b

( b

b

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

:: 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 )

( [[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

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 }

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

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

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;

for x, y being Element of R st x `1 = y `1 & x `2 = y `2 holds

x = y by Th94;

theorem :: MCART_1:96

proof end;

theorem :: MCART_1:97

proof end;