:: N-Tuples and Cartesian Products for n=5
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 13, 1990
:: Copyright (c) 1990 Association of Mizar Users
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]
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]
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]
theorem :: MCART_2:1
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y holds
Y1 misses X ) )
theorem Th2: :: MCART_2:2
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y holds
Y1 misses X ) )
definition
let x1,
x2,
x3,
x4,
x5 be
set ;
func [x1,x2,x3,x4,x5] -> set equals :: MCART_2:def 1
[[x1,x2,x3,x4],x5];
correctness
coherence
[[x1,x2,x3,x4],x5] is set ;
;
end;
:: deftheorem defines [ MCART_2:def 1 :
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5];
theorem Th3: :: MCART_2:3
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5]
theorem :: MCART_2:4
canceled;
theorem :: MCART_2:5
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5]
theorem Th6: :: MCART_2:6
for
x1,
x2,
x3,
x4,
x5 being
set holds
[x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5]
theorem Th7: :: MCART_2:7
for
x1,
x2,
x3,
x4,
x5,
y1,
y2,
y3,
y4,
y5 being
set st
[x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 &
x5 = y5 )
theorem Th8: :: MCART_2:8
for
X being
set st
X <> {} holds
ex
x being
set st
(
x in X & ( for
x1,
x2,
x3,
x4,
x5 being
set holds
( ( not
x1 in X & not
x2 in X ) or not
x = [x1,x2,x3,x4,x5] ) ) )
definition
let X1,
X2,
X3,
X4,
X5 be
set ;
func [:X1,X2,X3,X4,X5:] -> set equals :: MCART_2:def 2
[:[:X1,X2,X3,X4:],X5:];
correctness
coherence
[:[:X1,X2,X3,X4:],X5:] is set ;
;
end;
:: deftheorem defines [: MCART_2:def 2 :
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3,X4:],X5:];
theorem Th9: :: MCART_2:9
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:]
theorem :: MCART_2:10
canceled;
theorem :: MCART_2:11
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:]
theorem Th12: :: MCART_2:12
for
X1,
X2,
X3,
X4,
X5 being
set holds
[:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:]
theorem Th13: :: MCART_2:13
theorem Th14: :: MCART_2:14
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
[:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 )
theorem :: MCART_2:15
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
[:X1,X2,X3,X4,X5:] <> {} &
[:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 )
theorem :: MCART_2:16
theorem Th17: :: MCART_2:17
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] ex
xx1 being
Element of
X1 ex
xx2 being
Element of
X2 ex
xx3 being
Element of
X3 ex
xx4 being
Element of
X4 ex
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5]
definition
let X1,
X2,
X3,
X4,
X5 be
set ;
assume A1:
(
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} )
;
let x be
Element of
[:X1,X2,X3,X4,X5:];
func x `1 -> Element of
X1 means :
Def3:
:: MCART_2:def 3
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x1
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x1 ) holds
b1 = b2
func x `2 -> Element of
X2 means :
Def4:
:: MCART_2:def 4
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x2
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x2 ) holds
b1 = b2
func x `3 -> Element of
X3 means :
Def5:
:: MCART_2:def 5
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x3
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x3 ) holds
b1 = b2
func x `4 -> Element of
X4 means :
Def6:
:: MCART_2:def 6
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x4
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x4 ) holds
b1 = b2
func x `5 -> Element of
X5 means :
Def7:
:: MCART_2:def 7
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x5
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5 being set st x = [x1,x2,x3,x4,x5] holds
b2 = x5 ) holds
b1 = b2
end;
:: deftheorem Def3 defines `1 MCART_2:def 3 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X1 holds
(
b7 = x `1 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x1 );
:: deftheorem Def4 defines `2 MCART_2:def 4 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X2 holds
(
b7 = x `2 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x2 );
:: deftheorem Def5 defines `3 MCART_2:def 5 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X3 holds
(
b7 = x `3 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x3 );
:: deftheorem Def6 defines `4 MCART_2:def 6 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X4 holds
(
b7 = x `4 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x4 );
:: deftheorem Def7 defines `5 MCART_2:def 7 :
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
b7 being
Element of
X5 holds
(
b7 = x `5 iff for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
b7 = x5 );
theorem :: MCART_2:18
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 )
by Def3, Def4, Def5, Def6, Def7;
theorem Th19: :: MCART_2:19
for
X1,
X2,
X3,
X4,
X5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] holds
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )]
theorem Th20: :: MCART_2:20
theorem Th21: :: MCART_2:21
for
X1,
X2,
X3,
X4,
X5 being
set st (
X1 c= [:X1,X2,X3,X4,X5:] or
X1 c= [:X2,X3,X4,X5,X1:] or
X1 c= [:X3,X4,X5,X1,X2:] or
X1 c= [:X4,X5,X1,X2,X3:] or
X1 c= [:X5,X1,X2,X3,X4:] ) holds
X1 = {}
theorem :: MCART_2:22
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
[:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] holds
(
X1 meets Y1 &
X2 meets Y2 &
X3 meets Y3 &
X4 meets Y4 &
X5 meets Y5 )
theorem Th23: :: MCART_2:23
for
x1,
x2,
x3,
x4,
x5 being
set holds
[:{x1},{x2},{x3},{x4},{x5}:] = {[x1,x2,x3,x4,x5]}
theorem :: MCART_2:24
for
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} holds
for
x1,
x2,
x3,
x4,
x5 being
set st
x = [x1,x2,x3,x4,x5] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 )
by Def3, Def4, Def5, Def6, Def7;
theorem :: MCART_2:25
for
y1,
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y1 = xx1 ) holds
y1 = x `1
theorem :: MCART_2:26
for
y2,
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y2 = xx2 ) holds
y2 = x `2
theorem :: MCART_2:27
for
y3,
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y3 = xx3 ) holds
y3 = x `3
theorem :: MCART_2:28
for
y4,
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y4 = xx4 ) holds
y4 = x `4
theorem :: MCART_2:29
for
y5,
X1,
X2,
X3,
X4,
X5 being
set for
x being
Element of
[:X1,X2,X3,X4,X5:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 st
x = [xx1,xx2,xx3,xx4,xx5] holds
y5 = xx5 ) holds
y5 = x `5
theorem Th30: :: MCART_2:30
for
y,
X1,
X2,
X3,
X4,
X5 being
set st
y in [:X1,X2,X3,X4,X5:] holds
ex
x1,
x2,
x3,
x4,
x5 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
y = [x1,x2,x3,x4,x5] )
theorem Th31: :: MCART_2:31
for
x1,
x2,
x3,
x4,
x5,
X1,
X2,
X3,
X4,
X5 being
set holds
(
[x1,x2,x3,x4,x5] in [:X1,X2,X3,X4,X5:] iff (
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 ) )
theorem :: MCART_2:32
for
X1,
X2,
X3,
X4,
X5,
Z being
set st ( for
y being
set holds
(
y in Z iff ex
x1,
x2,
x3,
x4,
x5 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
y = [x1,x2,x3,x4,x5] ) ) ) holds
Z = [:X1,X2,X3,X4,X5:]
theorem Th33: :: MCART_2:33
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
Y1 <> {} &
Y2 <> {} &
Y3 <> {} &
Y4 <> {} &
Y5 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5:] for
y being
Element of
[:Y1,Y2,Y3,Y4,Y5:] st
x = y holds
(
x `1 = y `1 &
x `2 = y `2 &
x `3 = y `3 &
x `4 = y `4 &
x `5 = y `5 )
theorem :: MCART_2:34
for
X1,
X2,
X3,
X4,
X5 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
A5 being
Subset of
X5 for
x being
Element of
[:X1,X2,X3,X4,X5:] st
x in [:A1,A2,A3,A4,A5:] holds
(
x `1 in A1 &
x `2 in A2 &
x `3 in A3 &
x `4 in A4 &
x `5 in A5 )
theorem Th35: :: MCART_2:35
for
X1,
X2,
X3,
X4,
X5,
Y1,
Y2,
Y3,
Y4,
Y5 being
set st
X1 c= Y1 &
X2 c= Y2 &
X3 c= Y3 &
X4 c= Y4 &
X5 c= Y5 holds
[:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:]
definition
let X1,
X2,
X3,
X4,
X5 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;
let A5 be
Subset of
X5;
:: original: [:redefine func [:A1,A2,A3,A4,A5:] -> Subset of
[:X1,X2,X3,X4,X5:];
coherence
[:A1,A2,A3,A4,A5:] is Subset of [:X1,X2,X3,X4,X5:]
by Th35;
end;
theorem :: MCART_2:36
theorem :: MCART_2:37
theorem :: MCART_2:38
theorem :: MCART_2:39
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8 being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y holds
Y1 misses X ) )
theorem Th40: :: MCART_2:40
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9 being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in Y holds
Y1 misses X ) )
definition
let x1,
x2,
x3,
x4,
x5,
x6 be
set ;
func [x1,x2,x3,x4,x5,x6] -> set equals :: MCART_2:def 8
[[x1,x2,x3,x4,x5],x6];
correctness
coherence
[[x1,x2,x3,x4,x5],x6] is set ;
;
end;
:: deftheorem defines [ MCART_2:def 8 :
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
[x1,x2,x3,x4,x5,x6] = [[x1,x2,x3,x4,x5],x6];
theorem Th41: :: MCART_2:41
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
[x1,x2,x3,x4,x5,x6] = [[[[[x1,x2],x3],x4],x5],x6]
theorem :: MCART_2:42
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
[x1,x2,x3,x4,x5,x6] = [[x1,x2,x3,x4],x5,x6] by MCART_1:def 3;
theorem :: MCART_2:43
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
[x1,x2,x3,x4,x5,x6] = [[x1,x2,x3],x4,x5,x6]
theorem :: MCART_2:44
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
[x1,x2,x3,x4,x5,x6] = [[x1,x2],x3,x4,x5,x6] by Th6;
theorem Th45: :: MCART_2:45
for
x1,
x2,
x3,
x4,
x5,
x6,
y1,
y2,
y3,
y4,
y5,
y6 being
set st
[x1,x2,x3,x4,x5,x6] = [y1,y2,y3,y4,y5,y6] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 &
x5 = y5 &
x6 = y6 )
theorem Th46: :: MCART_2:46
for
X being
set st
X <> {} holds
ex
v being
set st
(
v in X & ( for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
( ( not
x1 in X & not
x2 in X ) or not
v = [x1,x2,x3,x4,x5,x6] ) ) )
definition
let X1,
X2,
X3,
X4,
X5,
X6 be
set ;
func [:X1,X2,X3,X4,X5,X6:] -> set equals :: MCART_2:def 9
[:[:X1,X2,X3,X4,X5:],X6:];
coherence
[:[:X1,X2,X3,X4,X5:],X6:] is set
;
end;
:: deftheorem defines [: MCART_2:def 9 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
[:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3,X4,X5:],X6:];
theorem Th47: :: MCART_2:47
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
[:X1,X2,X3,X4,X5,X6:] = [:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:]
theorem :: MCART_2:48
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
[:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3,X4:],X5,X6:] by ZFMISC_1:def 3;
theorem :: MCART_2:49
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
[:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2,X3:],X4,X5,X6:]
theorem :: MCART_2:50
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
[:X1,X2,X3,X4,X5,X6:] = [:[:X1,X2:],X3,X4,X5,X6:] by Th12;
theorem Th51: :: MCART_2:51
for
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
( (
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} ) iff
[:X1,X2,X3,X4,X5,X6:] <> {} )
theorem Th52: :: MCART_2:52
for
X1,
X2,
X3,
X4,
X5,
X6,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
[:X1,X2,X3,X4,X5,X6:] = [:Y1,Y2,Y3,Y4,Y5,Y6:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 )
theorem :: MCART_2:53
for
X1,
X2,
X3,
X4,
X5,
X6,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
[:X1,X2,X3,X4,X5,X6:] <> {} &
[:X1,X2,X3,X4,X5,X6:] = [:Y1,Y2,Y3,Y4,Y5,Y6:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 )
theorem :: MCART_2:54
for
X,
Y being
set st
[:X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y:] holds
X = Y
theorem Th55: :: MCART_2:55
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] ex
xx1 being
Element of
X1 ex
xx2 being
Element of
X2 ex
xx3 being
Element of
X3 ex
xx4 being
Element of
X4 ex
xx5 being
Element of
X5 ex
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6]
definition
let X1,
X2,
X3,
X4,
X5,
X6 be
set ;
assume A1:
(
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} )
;
let x be
Element of
[:X1,X2,X3,X4,X5,X6:];
func x `1 -> Element of
X1 means :
Def10:
:: MCART_2:def 10
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x1
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x1 ) holds
b1 = b2
func x `2 -> Element of
X2 means :
Def11:
:: MCART_2:def 11
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x2
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x2 ) holds
b1 = b2
func x `3 -> Element of
X3 means :
Def12:
:: MCART_2:def 12
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x3
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x3 ) holds
b1 = b2
func x `4 -> Element of
X4 means :
Def13:
:: MCART_2:def 13
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x4
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x4 ) holds
b1 = b2
func x `5 -> Element of
X5 means :
Def14:
:: MCART_2:def 14
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x5
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x5 ) holds
b1 = b2
func x `6 -> Element of
X6 means :
Def15:
:: MCART_2:def 15
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
it = x6;
existence
ex b1 being Element of X6 st
for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x6
uniqueness
for b1, b2 being Element of X6 st ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6 being set st x = [x1,x2,x3,x4,x5,x6] holds
b2 = x6 ) holds
b1 = b2
end;
:: deftheorem Def10 defines `1 MCART_2:def 10 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
b8 being
Element of
X1 holds
(
b8 = x `1 iff for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
b8 = x1 );
:: deftheorem Def11 defines `2 MCART_2:def 11 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
b8 being
Element of
X2 holds
(
b8 = x `2 iff for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
b8 = x2 );
:: deftheorem Def12 defines `3 MCART_2:def 12 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
b8 being
Element of
X3 holds
(
b8 = x `3 iff for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
b8 = x3 );
:: deftheorem Def13 defines `4 MCART_2:def 13 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
b8 being
Element of
X4 holds
(
b8 = x `4 iff for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
b8 = x4 );
:: deftheorem Def14 defines `5 MCART_2:def 14 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
b8 being
Element of
X5 holds
(
b8 = x `5 iff for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
b8 = x5 );
:: deftheorem Def15 defines `6 MCART_2:def 15 :
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
b8 being
Element of
X6 holds
(
b8 = x `6 iff for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
b8 = x6 );
theorem :: MCART_2:56
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 )
by Def10, Def11, Def12, Def13, Def14, Def15;
theorem Th57: :: MCART_2:57
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] holds
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 ),(x `6 )]
theorem Th58: :: MCART_2:58
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] holds
(
x `1 = ((((x `1 ) `1 ) `1 ) `1 ) `1 &
x `2 = ((((x `1 ) `1 ) `1 ) `1 ) `2 &
x `3 = (((x `1 ) `1 ) `1 ) `2 &
x `4 = ((x `1 ) `1 ) `2 &
x `5 = (x `1 ) `2 &
x `6 = x `2 )
theorem Th59: :: MCART_2:59
for
X1,
X2,
X3,
X4,
X5,
X6 being
set st (
X1 c= [:X1,X2,X3,X4,X5,X6:] or
X1 c= [:X2,X3,X4,X5,X6,X1:] or
X1 c= [:X3,X4,X5,X6,X1,X2:] or
X1 c= [:X4,X5,X6,X1,X2,X3:] or
X1 c= [:X5,X6,X1,X2,X3,X4:] or
X1 c= [:X6,X1,X2,X3,X4,X5:] ) holds
X1 = {}
theorem :: MCART_2:60
for
X1,
X2,
X3,
X4,
X5,
X6,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
[:X1,X2,X3,X4,X5,X6:] meets [:Y1,Y2,Y3,Y4,Y5,Y6:] holds
(
X1 meets Y1 &
X2 meets Y2 &
X3 meets Y3 &
X4 meets Y4 &
X5 meets Y5 &
X6 meets Y6 )
theorem Th61: :: MCART_2:61
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
[:{x1},{x2},{x3},{x4},{x5},{x6}:] = {[x1,x2,x3,x4,x5,x6]}
theorem :: MCART_2:62
for
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} holds
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x = [x1,x2,x3,x4,x5,x6] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 )
by Def10, Def11, Def12, Def13, Def14, Def15;
theorem :: MCART_2:63
for
y1,
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6] holds
y1 = xx1 ) holds
y1 = x `1
theorem :: MCART_2:64
for
y2,
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6] holds
y2 = xx2 ) holds
y2 = x `2
theorem :: MCART_2:65
for
y3,
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6] holds
y3 = xx3 ) holds
y3 = x `3
theorem :: MCART_2:66
for
y4,
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6] holds
y4 = xx4 ) holds
y4 = x `4
theorem :: MCART_2:67
for
y5,
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6] holds
y5 = xx5 ) holds
y5 = x `5
theorem :: MCART_2:68
for
y6,
X1,
X2,
X3,
X4,
X5,
X6 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 st
x = [xx1,xx2,xx3,xx4,xx5,xx6] holds
y6 = xx6 ) holds
y6 = x `6
theorem Th69: :: MCART_2:69
for
z,
X1,
X2,
X3,
X4,
X5,
X6 being
set st
z in [:X1,X2,X3,X4,X5,X6:] holds
ex
x1,
x2,
x3,
x4,
x5,
x6 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
z = [x1,x2,x3,x4,x5,x6] )
theorem Th70: :: MCART_2:70
for
x1,
x2,
x3,
x4,
x5,
x6,
X1,
X2,
X3,
X4,
X5,
X6 being
set holds
(
[x1,x2,x3,x4,x5,x6] in [:X1,X2,X3,X4,X5,X6:] iff (
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 ) )
theorem :: MCART_2:71
for
X1,
X2,
X3,
X4,
X5,
X6,
Z being
set st ( for
z being
set holds
(
z in Z iff ex
x1,
x2,
x3,
x4,
x5,
x6 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
z = [x1,x2,x3,x4,x5,x6] ) ) ) holds
Z = [:X1,X2,X3,X4,X5,X6:]
theorem Th72: :: MCART_2:72
for
X1,
X2,
X3,
X4,
X5,
X6,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
Y1 <> {} &
Y2 <> {} &
Y3 <> {} &
Y4 <> {} &
Y5 <> {} &
Y6 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] for
y being
Element of
[:Y1,Y2,Y3,Y4,Y5,Y6:] st
x = y holds
(
x `1 = y `1 &
x `2 = y `2 &
x `3 = y `3 &
x `4 = y `4 &
x `5 = y `5 &
x `6 = y `6 )
theorem :: MCART_2:73
for
X1,
X2,
X3,
X4,
X5,
X6 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
x being
Element of
[:X1,X2,X3,X4,X5,X6:] st
x in [:A1,A2,A3,A4,A5,A6:] holds
(
x `1 in A1 &
x `2 in A2 &
x `3 in A3 &
x `4 in A4 &
x `5 in A5 &
x `6 in A6 )
theorem Th74: :: MCART_2:74
for
X1,
X2,
X3,
X4,
X5,
X6,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6 being
set st
X1 c= Y1 &
X2 c= Y2 &
X3 c= Y3 &
X4 c= Y4 &
X5 c= Y5 &
X6 c= Y6 holds
[:X1,X2,X3,X4,X5,X6:] c= [:Y1,Y2,Y3,Y4,Y5,Y6:]
theorem :: MCART_2:75
for
X1,
X2,
X3,
X4,
X5,
X6 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 holds
[:A1,A2,A3,A4,A5,A6:] is
Subset of
[:X1,X2,X3,X4,X5,X6:] by Th74;
theorem :: MCART_2:76
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9,
YA being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in YA &
YA in Y holds
Y1 misses X ) )
theorem Th77: :: MCART_2:77
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9,
YA,
YB being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in YA &
YA in YB &
YB in Y holds
Y1 misses X ) )
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
set ;
func [x1,x2,x3,x4,x5,x6,x7] -> set equals :: MCART_2:def 16
[[x1,x2,x3,x4,x5,x6],x7];
correctness
coherence
[[x1,x2,x3,x4,x5,x6],x7] is set ;
;
end;
:: deftheorem defines [ MCART_2:def 16 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3,x4,x5,x6],x7];
theorem Th78: :: MCART_2:78
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[x1,x2,x3,x4,x5,x6,x7] = [[[[[[x1,x2],x3],x4],x5],x6],x7]
theorem :: MCART_2:79
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3,x4,x5],x6,x7] by MCART_1:def 3;
theorem :: MCART_2:80
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3,x4],x5,x6,x7] by MCART_1:31;
theorem :: MCART_2:81
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[x1,x2,x3,x4,x5,x6,x7] = [[x1,x2,x3],x4,x5,x6,x7]
theorem :: MCART_2:82
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[x1,x2,x3,x4,x5,x6,x7] = [[x1,x2],x3,x4,x5,x6,x7] by Th6;
theorem Th83: :: MCART_2:83
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
y1,
y2,
y3,
y4,
y5,
y6,
y7 being
set st
[x1,x2,x3,x4,x5,x6,x7] = [y1,y2,y3,y4,y5,y6,y7] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 &
x5 = y5 &
x6 = y6 &
x7 = y7 )
theorem Th84: :: MCART_2:84
for
X being
set st
X <> {} holds
ex
x being
set st
(
x in X & ( for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
( ( not
x1 in X & not
x2 in X ) or not
x = [x1,x2,x3,x4,x5,x6,x7] ) ) )
definition
let X1,
X2,
X3,
X4,
X5,
X6,
X7 be
set ;
func [:X1,X2,X3,X4,X5,X6,X7:] -> set equals :: MCART_2:def 17
[:[:X1,X2,X3,X4,X5,X6:],X7:];
correctness
coherence
[:[:X1,X2,X3,X4,X5,X6:],X7:] is set ;
;
end;
:: deftheorem defines [: MCART_2:def 17 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
[:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4,X5,X6:],X7:];
theorem Th85: :: MCART_2:85
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
[:X1,X2,X3,X4,X5,X6,X7:] = [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:]
theorem :: MCART_2:86
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
[:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4,X5:],X6,X7:] by ZFMISC_1:def 3;
theorem :: MCART_2:87
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
[:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4:],X5,X6,X7:] by MCART_1:53;
theorem :: MCART_2:88
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
[:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3:],X4,X5,X6,X7:]
theorem :: MCART_2:89
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
[:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2:],X3,X4,X5,X6,X7:] by Th12;
theorem Th90: :: MCART_2:90
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
( (
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} ) iff
[:X1,X2,X3,X4,X5,X6,X7:] <> {} )
theorem Th91: :: MCART_2:91
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
[:X1,X2,X3,X4,X5,X6,X7:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 &
X7 = Y7 )
theorem :: MCART_2:92
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
[:X1,X2,X3,X4,X5,X6,X7:] <> {} &
[:X1,X2,X3,X4,X5,X6,X7:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 &
X7 = Y7 )
theorem :: MCART_2:93
for
X,
Y being
set st
[:X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
theorem Th94: :: MCART_2:94
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] ex
xx1 being
Element of
X1 ex
xx2 being
Element of
X2 ex
xx3 being
Element of
X3 ex
xx4 being
Element of
X4 ex
xx5 being
Element of
X5 ex
xx6 being
Element of
X6 ex
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7]
definition
let X1,
X2,
X3,
X4,
X5,
X6,
X7 be
set ;
assume A1:
(
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} )
;
let x be
Element of
[:X1,X2,X3,X4,X5,X6,X7:];
func x `1 -> Element of
X1 means :
Def18:
:: MCART_2:def 18
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x1
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x1 ) holds
b1 = b2
func x `2 -> Element of
X2 means :
Def19:
:: MCART_2:def 19
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x2
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x2 ) holds
b1 = b2
func x `3 -> Element of
X3 means :
Def20:
:: MCART_2:def 20
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x3
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x3 ) holds
b1 = b2
func x `4 -> Element of
X4 means :
Def21:
:: MCART_2:def 21
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x4
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x4 ) holds
b1 = b2
func x `5 -> Element of
X5 means :
Def22:
:: MCART_2:def 22
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x5
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x5 ) holds
b1 = b2
func x `6 -> Element of
X6 means :
Def23:
:: MCART_2:def 23
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x6;
existence
ex b1 being Element of X6 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x6
uniqueness
for b1, b2 being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x6 ) holds
b1 = b2
func x `7 -> Element of
X7 means :
Def24:
:: MCART_2:def 24
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
it = x7;
existence
ex b1 being Element of X7 st
for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x7
uniqueness
for b1, b2 being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b1 = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7 being set st x = [x1,x2,x3,x4,x5,x6,x7] holds
b2 = x7 ) holds
b1 = b2
end;
:: deftheorem Def18 defines `1 MCART_2:def 18 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X1 holds
(
b9 = x `1 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x1 );
:: deftheorem Def19 defines `2 MCART_2:def 19 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X2 holds
(
b9 = x `2 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x2 );
:: deftheorem Def20 defines `3 MCART_2:def 20 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X3 holds
(
b9 = x `3 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x3 );
:: deftheorem Def21 defines `4 MCART_2:def 21 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X4 holds
(
b9 = x `4 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x4 );
:: deftheorem Def22 defines `5 MCART_2:def 22 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X5 holds
(
b9 = x `5 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x5 );
:: deftheorem Def23 defines `6 MCART_2:def 23 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X6 holds
(
b9 = x `6 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x6 );
:: deftheorem Def24 defines `7 MCART_2:def 24 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
b9 being
Element of
X7 holds
(
b9 = x `7 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
b9 = x7 );
theorem :: MCART_2:95
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 &
x `7 = x7 )
by Def18, Def19, Def20, Def21, Def22, Def23, Def24;
theorem Th96: :: MCART_2:96
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] holds
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 ),(x `6 ),(x `7 )]
theorem Th97: :: MCART_2:97
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] holds
(
x `1 = (((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 &
x `2 = (((((x `1 ) `1 ) `1 ) `1 ) `1 ) `2 &
x `3 = ((((x `1 ) `1 ) `1 ) `1 ) `2 &
x `4 = (((x `1 ) `1 ) `1 ) `2 &
x `5 = ((x `1 ) `1 ) `2 &
x `6 = (x `1 ) `2 &
x `7 = x `2 )
theorem Th98: :: MCART_2:98
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st (
X1 c= [:X1,X2,X3,X4,X5,X6,X7:] or
X1 c= [:X2,X3,X4,X5,X6,X7,X1:] or
X1 c= [:X3,X4,X5,X6,X7,X1,X2:] or
X1 c= [:X4,X5,X6,X7,X1,X2,X3:] or
X1 c= [:X5,X6,X7,X1,X2,X3,X4:] or
X1 c= [:X6,X7,X1,X2,X3,X4,X5:] or
X1 c= [:X7,X1,X2,X3,X4,X5,X6:] ) holds
X1 = {}
theorem Th99: :: MCART_2:99
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
[:X1,X2,X3,X4,X5,X6,X7:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] holds
(
X1 meets Y1 &
X2 meets Y2 &
X3 meets Y3 &
X4 meets Y4 &
X5 meets Y5 &
X6 meets Y6 &
X7 meets Y7 )
theorem Th100: :: MCART_2:100
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
[:{x1},{x2},{x3},{x4},{x5},{x6},{x7}:] = {[x1,x2,x3,x4,x5,x6,x7]}
theorem :: MCART_2:101
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} holds
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x = [x1,x2,x3,x4,x5,x6,x7] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 &
x `7 = x7 )
by Def18, Def19, Def20, Def21, Def22, Def23, Def24;
theorem :: MCART_2:102
for
y1,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y1 = xx1 ) holds
y1 = x `1
theorem :: MCART_2:103
for
y2,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y2 = xx2 ) holds
y2 = x `2
theorem :: MCART_2:104
for
y3,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y3 = xx3 ) holds
y3 = x `3
theorem :: MCART_2:105
for
y4,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y4 = xx4 ) holds
y4 = x `4
theorem :: MCART_2:106
for
y5,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y5 = xx5 ) holds
y5 = x `5
theorem :: MCART_2:107
for
y6,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y6 = xx6 ) holds
y6 = x `6
theorem :: MCART_2:108
for
y7,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] holds
y7 = xx7 ) holds
y7 = x `7
theorem Th109: :: MCART_2:109
for
y,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set st
y in [:X1,X2,X3,X4,X5,X6,X7:] holds
ex
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
y = [x1,x2,x3,x4,x5,x6,x7] )
theorem Th110: :: MCART_2:110
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
X1,
X2,
X3,
X4,
X5,
X6,
X7 being
set holds
(
[x1,x2,x3,x4,x5,x6,x7] in [:X1,X2,X3,X4,X5,X6,X7:] iff (
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 ) )
theorem :: MCART_2:111
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
Z being
set st ( for
y being
set holds
(
y in Z iff ex
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
y = [x1,x2,x3,x4,x5,x6,x7] ) ) ) holds
Z = [:X1,X2,X3,X4,X5,X6,X7:]
theorem Th112: :: MCART_2:112
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
Y1 <> {} &
Y2 <> {} &
Y3 <> {} &
Y4 <> {} &
Y5 <> {} &
Y6 <> {} &
Y7 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] for
y being
Element of
[:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] st
x = y holds
(
x `1 = y `1 &
x `2 = y `2 &
x `3 = y `3 &
x `4 = y `4 &
x `5 = y `5 &
x `6 = y `6 &
x `7 = y `7 )
theorem :: MCART_2:113
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
A7 being
Subset of
X7 for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7:] st
x in [:A1,A2,A3,A4,A5,A6,A7:] holds
(
x `1 in A1 &
x `2 in A2 &
x `3 in A3 &
x `4 in A4 &
x `5 in A5 &
x `6 in A6 &
x `7 in A7 )
theorem Th114: :: MCART_2:114
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7 being
set st
X1 c= Y1 &
X2 c= Y2 &
X3 c= Y3 &
X4 c= Y4 &
X5 c= Y5 &
X6 c= Y6 &
X7 c= Y7 holds
[:X1,X2,X3,X4,X5,X6,X7:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:]
theorem :: MCART_2:115
for
X1,
X2,
X3,
X4,
X5,
X6,
X7 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
A7 being
Subset of
X7 holds
[:A1,A2,A3,A4,A5,A6,A7:] is
Subset of
[:X1,X2,X3,X4,X5,X6,X7:] by Th114;
theorem :: MCART_2:116
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9,
YA,
YB,
YC being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in YA &
YA in YB &
YB in YC &
YC in Y holds
Y1 misses X ) )
theorem Th117: :: MCART_2:117
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9,
YA,
YB,
YC,
YD being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in YA &
YA in YB &
YB in YC &
YC in YD &
YD in Y holds
Y1 misses X ) )
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 be
set ;
func [x1,x2,x3,x4,x5,x6,x7,x8] -> set equals :: MCART_2:def 25
[[x1,x2,x3,x4,x5,x6,x7],x8];
correctness
coherence
[[x1,x2,x3,x4,x5,x6,x7],x8] is set ;
;
end;
:: deftheorem defines [ MCART_2:def 25 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6,x7],x8];
theorem :: MCART_2:118
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8]
theorem :: MCART_2:119
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6],x7,x8] by MCART_1:def 3;
theorem :: MCART_2:120
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5],x6,x7,x8] by MCART_1:31;
theorem :: MCART_2:121
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4],x5,x6,x7,x8] by Th3;
theorem :: MCART_2:122
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3],x4,x5,x6,x7,x8]
theorem :: MCART_2:123
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2],x3,x4,x5,x6,x7,x8] by Th6;
theorem Th124: :: MCART_2:124
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
y1,
y2,
y3,
y4,
y5,
y6,
y7,
y8 being
set st
[x1,x2,x3,x4,x5,x6,x7,x8] = [y1,y2,y3,y4,y5,y6,y7,y8] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 &
x5 = y5 &
x6 = y6 &
x7 = y7 &
x8 = y8 )
theorem Th125: :: MCART_2:125
for
X being
set st
X <> {} holds
ex
y being
set st
(
y in X & ( for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
( ( not
x1 in X & not
x2 in X ) or not
y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) )
definition
let X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 be
set ;
func [:X1,X2,X3,X4,X5,X6,X7,X8:] -> set equals :: MCART_2:def 26
[:[:X1,X2,X3,X4,X5,X6,X7:],X8:];
correctness
coherence
[:[:X1,X2,X3,X4,X5,X6,X7:],X8:] is set ;
;
end;
:: deftheorem defines [: MCART_2:def 26 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8:];
theorem Th126: :: MCART_2:126
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:]
theorem :: MCART_2:127
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6:],X7,X8:] by ZFMISC_1:def 3;
theorem :: MCART_2:128
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5:],X6,X7,X8:] by MCART_1:53;
theorem :: MCART_2:129
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8:] by Th9;
theorem :: MCART_2:130
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8:]
theorem :: MCART_2:131
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8:] by Th12;
theorem Th132: :: MCART_2:132
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
( (
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} ) iff
[:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} )
theorem Th133: :: MCART_2:133
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 &
X7 = Y7 &
X8 = Y8 )
theorem :: MCART_2:134
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8 being
set st
[:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} &
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 &
X7 = Y7 &
X8 = Y8 )
theorem :: MCART_2:135
for
X,
Y being
set st
[:X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
theorem Th136: :: MCART_2:136
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] ex
xx1 being
Element of
X1 ex
xx2 being
Element of
X2 ex
xx3 being
Element of
X3 ex
xx4 being
Element of
X4 ex
xx5 being
Element of
X5 ex
xx6 being
Element of
X6 ex
xx7 being
Element of
X7 ex
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8]
definition
let X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 be
set ;
assume A1:
(
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} )
;
let x be
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:];
func x `1 -> Element of
X1 means :
Def27:
:: MCART_2:def 27
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x1
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x1 ) holds
b1 = b2
func x `2 -> Element of
X2 means :
Def28:
:: MCART_2:def 28
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x2
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x2 ) holds
b1 = b2
func x `3 -> Element of
X3 means :
Def29:
:: MCART_2:def 29
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x3
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x3 ) holds
b1 = b2
func x `4 -> Element of
X4 means :
Def30:
:: MCART_2:def 30
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x4
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x4 ) holds
b1 = b2
func x `5 -> Element of
X5 means :
Def31:
:: MCART_2:def 31
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x5
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x5 ) holds
b1 = b2
func x `6 -> Element of
X6 means :
Def32:
:: MCART_2:def 32
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x6;
existence
ex b1 being Element of X6 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x6
uniqueness
for b1, b2 being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x6 ) holds
b1 = b2
func x `7 -> Element of
X7 means :
Def33:
:: MCART_2:def 33
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x7;
existence
ex b1 being Element of X7 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x7
uniqueness
for b1, b2 being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x7 ) holds
b1 = b2
func x `8 -> Element of
X8 means :
Def34:
:: MCART_2:def 34
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
it = x8;
existence
ex b1 being Element of X8 st
for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x8
uniqueness
for b1, b2 being Element of X8 st ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b1 = x8 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b2 = x8 ) holds
b1 = b2
end;
:: deftheorem Def27 defines `1 MCART_2:def 27 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X1 holds
(
b10 = x `1 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x1 );
:: deftheorem Def28 defines `2 MCART_2:def 28 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X2 holds
(
b10 = x `2 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x2 );
:: deftheorem Def29 defines `3 MCART_2:def 29 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X3 holds
(
b10 = x `3 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x3 );
:: deftheorem Def30 defines `4 MCART_2:def 30 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X4 holds
(
b10 = x `4 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x4 );
:: deftheorem Def31 defines `5 MCART_2:def 31 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X5 holds
(
b10 = x `5 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x5 );
:: deftheorem Def32 defines `6 MCART_2:def 32 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X6 holds
(
b10 = x `6 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x6 );
:: deftheorem Def33 defines `7 MCART_2:def 33 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X7 holds
(
b10 = x `7 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x7 );
:: deftheorem Def34 defines `8 MCART_2:def 34 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
b10 being
Element of
X8 holds
(
b10 = x `8 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
b10 = x8 );
theorem :: MCART_2:137
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 &
x `7 = x7 &
x `8 = x8 )
by Def27, Def28, Def29, Def30, Def31, Def32, Def33, Def34;
theorem Th138: :: MCART_2:138
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] holds
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 ),(x `6 ),(x `7 ),(x `8 )]
theorem Th139: :: MCART_2:139
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] holds
(
x `1 = ((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 &
x `2 = ((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 &
x `3 = (((((x `1 ) `1 ) `1 ) `1 ) `1 ) `2 &
x `4 = ((((x `1 ) `1 ) `1 ) `1 ) `2 &
x `5 = (((x `1 ) `1 ) `1 ) `2 &
x `6 = ((x `1 ) `1 ) `2 &
x `7 = (x `1 ) `2 &
x `8 = x `2 )
theorem :: MCART_2:140
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st (
X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] or
X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] or
X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] or
X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] or
X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] or
X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] or
X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] or
X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] ) holds
X1 = {}
theorem Th141: :: MCART_2:141
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8 being
set st
[:X1,X2,X3,X4,X5,X6,X7,X8:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds
(
X1 meets Y1 &
X2 meets Y2 &
X3 meets Y3 &
X4 meets Y4 &
X5 meets Y5 &
X6 meets Y6 &
X7 meets Y7 &
X8 meets Y8 )
theorem Th142: :: MCART_2:142
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
[:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8}:] = {[x1,x2,x3,x4,x5,x6,x7,x8]}
theorem :: MCART_2:143
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} holds
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 &
x `7 = x7 &
x `8 = x8 )
by Def27, Def28, Def29, Def30, Def31, Def32, Def33, Def34;
theorem :: MCART_2:144
for
y1,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y1 = xx1 ) holds
y1 = x `1
theorem :: MCART_2:145
for
y2,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y2 = xx2 ) holds
y2 = x `2
theorem :: MCART_2:146
for
y3,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y3 = xx3 ) holds
y3 = x `3
theorem :: MCART_2:147
for
y4,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y4 = xx4 ) holds
y4 = x `4
theorem :: MCART_2:148
for
y5,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y5 = xx5 ) holds
y5 = x `5
theorem :: MCART_2:149
for
y6,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y6 = xx6 ) holds
y6 = x `6
theorem :: MCART_2:150
for
y7,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y7 = xx7 ) holds
y7 = x `7
theorem :: MCART_2:151
for
y8,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds
y8 = xx8 ) holds
y8 = x `8
theorem Th152: :: MCART_2:152
for
y,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set st
y in [:X1,X2,X3,X4,X5,X6,X7,X8:] holds
ex
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
x8 in X8 &
y = [x1,x2,x3,x4,x5,x6,x7,x8] )
theorem Th153: :: MCART_2:153
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 being
set holds
(
[x1,x2,x3,x4,x5,x6,x7,x8] in [:X1,X2,X3,X4,X5,X6,X7,X8:] iff (
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
x8 in X8 ) )
theorem :: MCART_2:154
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
Z being
set st ( for
y being
set holds
(
y in Z iff ex
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
x8 in X8 &
y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) ) holds
Z = [:X1,X2,X3,X4,X5,X6,X7,X8:]
theorem Th155: :: MCART_2:155
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
Y1 <> {} &
Y2 <> {} &
Y3 <> {} &
Y4 <> {} &
Y5 <> {} &
Y6 <> {} &
Y7 <> {} &
Y8 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] for
y being
Element of
[:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] st
x = y holds
(
x `1 = y `1 &
x `2 = y `2 &
x `3 = y `3 &
x `4 = y `4 &
x `5 = y `5 &
x `6 = y `6 &
x `7 = y `7 &
x `8 = y `8 )
theorem :: MCART_2:156
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
A7 being
Subset of
X7 for
A8 being
Subset of
X8 for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8:] st
x in [:A1,A2,A3,A4,A5,A6,A7,A8:] holds
(
x `1 in A1 &
x `2 in A2 &
x `3 in A3 &
x `4 in A4 &
x `5 in A5 &
x `6 in A6 &
x `7 in A7 &
x `8 in A8 )
theorem Th157: :: MCART_2:157
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8 being
set st
X1 c= Y1 &
X2 c= Y2 &
X3 c= Y3 &
X4 c= Y4 &
X5 c= Y5 &
X6 c= Y6 &
X7 c= Y7 &
X8 c= Y8 holds
[:X1,X2,X3,X4,X5,X6,X7,X8:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]
theorem :: MCART_2:158
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
A7 being
Subset of
X7 for
A8 being
Subset of
X8 holds
[:A1,A2,A3,A4,A5,A6,A7,A8:] is
Subset of
[:X1,X2,X3,X4,X5,X6,X7,X8:] by Th157;
theorem :: MCART_2:159
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9,
YA,
YB,
YC,
YD,
YE being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in YA &
YA in YB &
YB in YC &
YC in YD &
YD in YE &
YE in Y holds
Y1 misses X ) )
theorem :: MCART_2:160
for
X being
set st
X <> {} holds
ex
Y being
set st
(
Y in X & ( for
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9,
YA,
YB,
YC,
YD,
YE,
YF being
set st
Y1 in Y2 &
Y2 in Y3 &
Y3 in Y4 &
Y4 in Y5 &
Y5 in Y6 &
Y6 in Y7 &
Y7 in Y8 &
Y8 in Y9 &
Y9 in YA &
YA in YB &
YB in YC &
YC in YD &
YD in YE &
YE in YF &
YF in Y holds
Y1 misses X ) )
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 be
set ;
func [x1,x2,x3,x4,x5,x6,x7,x8,x9] -> set equals :: MCART_2:def 35
[[x1,x2,x3,x4,x5,x6,x7,x8],x9];
coherence
[[x1,x2,x3,x4,x5,x6,x7,x8],x9] is set
;
end;
:: deftheorem defines [ MCART_2:def 35 :
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7,x8],x9];
theorem Th161: :: MCART_2:161
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[[[[[[[x1,x2],x3],x4],x5],x6],x7],x8],x9]
theorem :: MCART_2:162
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7],x8,x9] by MCART_1:def 3;
theorem :: MCART_2:163
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6],x7,x8,x9] by MCART_1:31;
theorem :: MCART_2:164
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5],x6,x7,x8,x9] by Th3;
theorem :: MCART_2:165
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4],x5,x6,x7,x8,x9] by Th41;
theorem :: MCART_2:166
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3],x4,x5,x6,x7,x8,x9]
theorem :: MCART_2:167
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2],x3,x4,x5,x6,x7,x8,x9] by Th6;
theorem Th168: :: MCART_2:168
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
y1,
y2,
y3,
y4,
y5,
y6,
y7,
y8,
y9 being
set st
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [y1,y2,y3,y4,y5,y6,y7,y8,y9] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 &
x5 = y5 &
x6 = y6 &
x7 = y7 &
x8 = y8 &
x9 = y9 )
definition
let X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 be
set ;
func [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] -> set equals :: MCART_2:def 36
[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];
coherence
[:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:] is set
;
end;
:: deftheorem defines [: MCART_2:def 36 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6,X7,X8:],X9:];
theorem Th169: :: MCART_2:169
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:]
theorem :: MCART_2:170
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8,X9:] by ZFMISC_1:def 3;
theorem :: MCART_2:171
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5,X6:],X7,X8,X9:] by MCART_1:53;
theorem :: MCART_2:172
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4,X5:],X6,X7,X8,X9:] by Th9;
theorem :: MCART_2:173
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8,X9:] by Th47;
theorem :: MCART_2:174
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8,X9:]
theorem :: MCART_2:175
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8,X9:] by Th12;
theorem Th176: :: MCART_2:176
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
( (
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} ) iff
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} )
theorem Th177: :: MCART_2:177
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} &
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 &
X7 = Y7 &
X8 = Y8 &
X9 = Y9 )
theorem :: MCART_2:178
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9 being
set st
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {} &
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds
(
X1 = Y1 &
X2 = Y2 &
X3 = Y3 &
X4 = Y4 &
X5 = Y5 &
X6 = Y6 &
X7 = Y7 &
X8 = Y8 &
X9 = Y9 )
theorem :: MCART_2:179
for
X,
Y being
set st
[:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] holds
X = Y
theorem Th180: :: MCART_2:180
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] ex
xx1 being
Element of
X1 ex
xx2 being
Element of
X2 ex
xx3 being
Element of
X3 ex
xx4 being
Element of
X4 ex
xx5 being
Element of
X5 ex
xx6 being
Element of
X6 ex
xx7 being
Element of
X7 ex
xx8 being
Element of
X8 ex
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9]
definition
let X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 be
set ;
assume A1:
(
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} )
;
let x be
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
func x `1 -> Element of
X1 means :
Def37:
:: MCART_2:def 37
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x1;
existence
ex b1 being Element of X1 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x1
uniqueness
for b1, b2 being Element of X1 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x1 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x1 ) holds
b1 = b2
func x `2 -> Element of
X2 means :
Def38:
:: MCART_2:def 38
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x2;
existence
ex b1 being Element of X2 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x2
uniqueness
for b1, b2 being Element of X2 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x2 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x2 ) holds
b1 = b2
func x `3 -> Element of
X3 means :
Def39:
:: MCART_2:def 39
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x3;
existence
ex b1 being Element of X3 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x3
uniqueness
for b1, b2 being Element of X3 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x3 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x3 ) holds
b1 = b2
func x `4 -> Element of
X4 means :
Def40:
:: MCART_2:def 40
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x4;
existence
ex b1 being Element of X4 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x4
uniqueness
for b1, b2 being Element of X4 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x4 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x4 ) holds
b1 = b2
func x `5 -> Element of
X5 means :
Def41:
:: MCART_2:def 41
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x5;
existence
ex b1 being Element of X5 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x5
uniqueness
for b1, b2 being Element of X5 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x5 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x5 ) holds
b1 = b2
func x `6 -> Element of
X6 means :
Def42:
:: MCART_2:def 42
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x6;
existence
ex b1 being Element of X6 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x6
uniqueness
for b1, b2 being Element of X6 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x6 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x6 ) holds
b1 = b2
func x `7 -> Element of
X7 means :
Def43:
:: MCART_2:def 43
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x7;
existence
ex b1 being Element of X7 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x7
uniqueness
for b1, b2 being Element of X7 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x7 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x7 ) holds
b1 = b2
func x `8 -> Element of
X8 means :
Def44:
:: MCART_2:def 44
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x8;
existence
ex b1 being Element of X8 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x8
uniqueness
for b1, b2 being Element of X8 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x8 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x8 ) holds
b1 = b2
func x `9 -> Element of
X9 means :
Def45:
:: MCART_2:def 45
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
it = x9;
existence
ex b1 being Element of X9 st
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x9
uniqueness
for b1, b2 being Element of X9 st ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b1 = x9 ) & ( for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b2 = x9 ) holds
b1 = b2
end;
:: deftheorem Def37 defines `1 MCART_2:def 37 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X1 holds
(
b11 = x `1 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x1 );
:: deftheorem Def38 defines `2 MCART_2:def 38 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X2 holds
(
b11 = x `2 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x2 );
:: deftheorem Def39 defines `3 MCART_2:def 39 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X3 holds
(
b11 = x `3 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x3 );
:: deftheorem Def40 defines `4 MCART_2:def 40 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X4 holds
(
b11 = x `4 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x4 );
:: deftheorem Def41 defines `5 MCART_2:def 41 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X5 holds
(
b11 = x `5 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x5 );
:: deftheorem Def42 defines `6 MCART_2:def 42 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X6 holds
(
b11 = x `6 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x6 );
:: deftheorem Def43 defines `7 MCART_2:def 43 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X7 holds
(
b11 = x `7 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x7 );
:: deftheorem Def44 defines `8 MCART_2:def 44 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X8 holds
(
b11 = x `8 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x8 );
:: deftheorem Def45 defines `9 MCART_2:def 45 :
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
b11 being
Element of
X9 holds
(
b11 = x `9 iff for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
b11 = x9 );
theorem :: MCART_2:181
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 &
x `7 = x7 &
x `8 = x8 &
x `9 = x9 )
by Def37, Def38, Def39, Def40, Def41, Def42, Def43, Def44, Def45;
theorem Th182: :: MCART_2:182
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 ),(x `6 ),(x `7 ),(x `8 ),(x `9 )]
theorem Th183: :: MCART_2:183
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
(
x `1 = (((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 &
x `2 = (((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 &
x `3 = ((((((x `1 ) `1 ) `1 ) `1 ) `1 ) `1 ) `2 &
x `4 = (((((x `1 ) `1 ) `1 ) `1 ) `1 ) `2 &
x `5 = ((((x `1 ) `1 ) `1 ) `1 ) `2 &
x `6 = (((x `1 ) `1 ) `1 ) `2 &
x `7 = ((x `1 ) `1 ) `2 &
x `8 = (x `1 ) `2 &
x `9 = x `2 )
theorem :: MCART_2:184
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9 being
set st
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] holds
(
X1 meets Y1 &
X2 meets Y2 &
X3 meets Y3 &
X4 meets Y4 &
X5 meets Y5 &
X6 meets Y6 &
X7 meets Y7 &
X8 meets Y8 &
X9 meets Y9 )
theorem :: MCART_2:185
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
[:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8},{x9}:] = {[x1,x2,x3,x4,x5,x6,x7,x8,x9]}
theorem :: MCART_2:186
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} holds
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] holds
(
x `1 = x1 &
x `2 = x2 &
x `3 = x3 &
x `4 = x4 &
x `5 = x5 &
x `6 = x6 &
x `7 = x7 &
x `8 = x8 &
x `9 = x9 )
by Def37, Def38, Def39, Def40, Def41, Def42, Def43, Def44, Def45;
theorem :: MCART_2:187
for
y1,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y1 = xx1 ) holds
y1 = x `1
theorem :: MCART_2:188
for
y2,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y2 = xx2 ) holds
y2 = x `2
theorem :: MCART_2:189
for
y3,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y3 = xx3 ) holds
y3 = x `3
theorem :: MCART_2:190
for
y4,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y4 = xx4 ) holds
y4 = x `4
theorem :: MCART_2:191
for
y5,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y5 = xx5 ) holds
y5 = x `5
theorem :: MCART_2:192
for
y6,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y6 = xx6 ) holds
y6 = x `6
theorem :: MCART_2:193
for
y7,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y7 = xx7 ) holds
y7 = x `7
theorem :: MCART_2:194
for
y8,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y8 = xx8 ) holds
y8 = x `8
theorem :: MCART_2:195
for
y9,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} & ( for
xx1 being
Element of
X1 for
xx2 being
Element of
X2 for
xx3 being
Element of
X3 for
xx4 being
Element of
X4 for
xx5 being
Element of
X5 for
xx6 being
Element of
X6 for
xx7 being
Element of
X7 for
xx8 being
Element of
X8 for
xx9 being
Element of
X9 st
x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds
y9 = xx9 ) holds
y9 = x `9
theorem :: MCART_2:196
for
y,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set st
y in [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
ex
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
x8 in X8 &
x9 in X9 &
y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] )
theorem :: MCART_2:197
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 being
set holds
(
[x1,x2,x3,x4,x5,x6,x7,x8,x9] in [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] iff (
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
x8 in X8 &
x9 in X9 ) )
theorem :: MCART_2:198
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9,
Z being
set st ( for
y being
set holds
(
y in Z iff ex
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set st
(
x1 in X1 &
x2 in X2 &
x3 in X3 &
x4 in X4 &
x5 in X5 &
x6 in X6 &
x7 in X7 &
x8 in X8 &
x9 in X9 &
y = [x1,x2,x3,x4,x5,x6,x7,x8,x9] ) ) ) holds
Z = [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
theorem Th199: :: MCART_2:199
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9 being
set st
X1 <> {} &
X2 <> {} &
X3 <> {} &
X4 <> {} &
X5 <> {} &
X6 <> {} &
X7 <> {} &
X8 <> {} &
X9 <> {} &
Y1 <> {} &
Y2 <> {} &
Y3 <> {} &
Y4 <> {} &
Y5 <> {} &
Y6 <> {} &
Y7 <> {} &
Y8 <> {} &
Y9 <> {} holds
for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] for
y being
Element of
[:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] st
x = y holds
(
x `1 = y `1 &
x `2 = y `2 &
x `3 = y `3 &
x `4 = y `4 &
x `5 = y `5 &
x `6 = y `6 &
x `7 = y `7 &
x `8 = y `8 &
x `9 = y `9 )
theorem :: MCART_2:200
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
A7 being
Subset of
X7 for
A8 being
Subset of
X8 for
A9 being
Subset of
X9 for
x being
Element of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] st
x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:] holds
(
x `1 in A1 &
x `2 in A2 &
x `3 in A3 &
x `4 in A4 &
x `5 in A5 &
x `6 in A6 &
x `7 in A7 &
x `8 in A8 &
x `9 in A9 )
theorem Th201: :: MCART_2:201
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9,
Y1,
Y2,
Y3,
Y4,
Y5,
Y6,
Y7,
Y8,
Y9 being
set st
X1 c= Y1 &
X2 c= Y2 &
X3 c= Y3 &
X4 c= Y4 &
X5 c= Y5 &
X6 c= Y6 &
X7 c= Y7 &
X8 c= Y8 &
X9 c= Y9 holds
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
theorem :: MCART_2:202
for
X1,
X2,
X3,
X4,
X5,
X6,
X7,
X8,
X9 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
A5 being
Subset of
X5 for
A6 being
Subset of
X6 for
A7 being
Subset of
X7 for
A8 being
Subset of
X8 for
A9 being
Subset of
X9 holds
[:A1,A2,A3,A4,A5,A6,A7,A8,A9:] is
Subset of
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] by Th201;