let a be object ; :: thesis: for X, Y, Z being set holds
( a in product <*X,Y,Z*> iff ex x, y, z being object st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) )
let X, Y, Z be set ; :: thesis: ( a in product <*X,Y,Z*> iff ex x, y, z being object st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) )
A1: 3 in Seg 3 by Th1, ENUMSET1:def 1;
A2: ( <*X,Y,Z*> . 1 = X & <*X,Y,Z*> . 2 = Y ) by FINSEQ_1:45;
A3: <*X,Y,Z*> . 3 = Z by FINSEQ_1:45;
len <*X,Y,Z*> = 3 by FINSEQ_1:45;
then A4: dom <*X,Y,Z*> = Seg 3 by FINSEQ_1:def 3;
A5: ( 1 in Seg 3 & 2 in Seg 3 ) by Th1, ENUMSET1:def 1;
thus ( a in product <*X,Y,Z*> implies ex x, y, z being object st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) ) :: thesis: ( ex x, y, z being object st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) implies a in product <*X,Y,Z*> )
proof
assume a in product <*X,Y,Z*> ; :: thesis: ex x, y, z being object st
( x in X & y in Y & z in Z & a = <*x,y,z*> )
then consider f being Function such that
A6: a = f and
A7: dom f = dom <*X,Y,Z*> and
A8: for x being object st x in dom <*X,Y,Z*> holds
f . x in <*X,Y,Z*> . x by CARD_3:def 5;
reconsider f = f as FinSequence by A4, A7, FINSEQ_1:def 2;
take f . 1 ; :: thesis: ex y, z being object st
( f . 1 in X & y in Y & z in Z & a = <*(f . 1),y,z*> )
take f . 2 ; :: thesis: ex z being object st
( f . 1 in X & f . 2 in Y & z in Z & a = <*(f . 1),(f . 2),z*> )
take f . 3 ; :: thesis: ( f . 1 in X & f . 2 in Y & f . 3 in Z & a = <*(f . 1),(f . 2),(f . 3)*> )
len f = 3 by A4, A7, FINSEQ_1:def 3;
hence ( f . 1 in X & f . 2 in Y & f . 3 in Z & a = <*(f . 1),(f . 2),(f . 3)*> ) by A4, A5, A1, A2, A3, A6, A8, FINSEQ_1:45; :: thesis: verum
end;
given x, y, z being object such that A9: ( x in X & y in Y & z in Z ) and
A10: a = <*x,y,z*> ; :: thesis: a in product <*X,Y,Z*>
A11: now :: thesis: for a being object st a in Seg 3 holds
<*x,y,z*> . a in <*X,Y,Z*> . a
let a be object ; :: thesis: ( a in Seg 3 implies <*x,y,z*> . a in <*X,Y,Z*> . a )
assume a in Seg 3 ; :: thesis: <*x,y,z*> . a in <*X,Y,Z*> . a
then ( a = 1 or a = 2 or a = 3 ) by Th1, ENUMSET1:def 1;
hence <*x,y,z*> . a in <*X,Y,Z*> . a by A2, A3, A9, FINSEQ_1:45; :: thesis: verum
end;
len <*x,y,z*> = 3 by FINSEQ_1:45;
then dom <*x,y,z*> = Seg 3 by FINSEQ_1:def 3;
hence a in product <*X,Y,Z*> by A4, A10, A11, CARD_3:def 5; :: thesis: verum