let x, X be set ; :: thesis: ( x in product <*X*> iff ex y being set st
( y in X & x = <*y*> ) )
A1: ( dom <*X*> = Seg 1 & 1 in Seg 1 & <*X*> . 1 = X ) by FINSEQ_1:4, FINSEQ_1:def 8, TARSKI:def 1;
thus ( x in product <*X*> implies ex y being set st
( y in X & x = <*y*> ) ) :: thesis: ( ex y being set st
( y in X & x = <*y*> ) implies x in product <*X*> )

proof

assume x in product <*X*> ; :: thesis: ex y being set st
( y in X & x = <*y*> )
then consider f being Function such that
A2: ( x = f & dom f = dom <*X*> & ( for x being set st x in dom <*X*> holds
f . x in <*X*> . x ) ) by CARD_3:def 5;
reconsider f = f as FinSequence by A1, A2, FINSEQ_1:def 2;
take f . 1 ; :: thesis: ( f . 1 in X & x = <*(f . 1)*> )
thus ( f . 1 in X & x = <*(f . 1)*> ) by A1, A2, FINSEQ_1:def 8; :: thesis: verum

end;

given y being set such that A3: ( y in X & x = <*y*> ) ; :: thesis: x in product <*X*>
A4: dom <*y*> = Seg 1 by FINSEQ_1:def 8;

now

let a be set ; :: thesis: ( a in Seg 1 implies <*y*> . a in <*X*> . a )
assume a in Seg 1 ; :: thesis: <*y*> . a in <*X*> . a
then a = 1 by FINSEQ_1:4, TARSKI:def 1;
hence <*y*> . a in <*X*> . a by A1, A3, FINSEQ_1:def 8; :: thesis: verum

end;

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