let z, X, Y be set ; :: thesis: ( z in product <*X,Y*> iff ex x, y being set st
( x in X & y in Y & z = <*x,y*> ) )
len <*X,Y*> = 2 by FINSEQ_1:61;
then A1: ( dom <*X,Y*> = Seg 2 & 1 in Seg 2 & 2 in Seg 2 & <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by FINSEQ_1:4, FINSEQ_1:61, FINSEQ_1:def 3, TARSKI:def 2;
thus ( z in product <*X,Y*> implies ex x, y being set st
( x in X & y in Y & z = <*x,y*> ) ) :: thesis: ( ex x, y being set 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 set st
( x in X & y in Y & z = <*x,y*> )
then consider f being Function such that
A2: ( z = f & dom f = dom <*X,Y*> & ( for x being set st x in dom <*X,Y*> holds
f . x in <*X,Y*> . x ) ) by CARD_3:def 5;
reconsider f = f as FinSequence by A1, A2, FINSEQ_1:def 2;
take f . 1 ; :: thesis: ex y being set 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 A1, A2, FINSEQ_1:def 3;
hence ( f . 1 in X & f . 2 in Y & z = <*(f . 1),(f . 2)*> ) by A1, A2, FINSEQ_1:61; :: thesis: verum

end;

given x, y being set such that A3: ( x in X & y in Y & z = <*x,y*> ) ; :: thesis: z in product <*X,Y*>
len <*x,y*> = 2 by FINSEQ_1:61;
then A4: dom <*x,y*> = Seg 2 by FINSEQ_1:def 3;

now

let a be set ; :: 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:4, TARSKI:def 2;
hence <*x,y*> . a in <*X,Y*> . a by A1, A3, FINSEQ_1:61; :: thesis: verum

end;

hence z in product <*X,Y*> by A1, A3, A4, CARD_3:def 5; :: thesis: verum