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