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

proof

assume x in product <*X*> ; :: thesis: ex y being object st
( y in X & x = <*y*> )
then consider f being Function such that
A4: x = f and
A5: dom f = dom <*X*> and
A6: for x being object st x in dom <*X*> holds
f . x in <*X*> . x by CARD_3:def 5;
reconsider f = f as FinSequence by A1, A5, 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, A3, A2, A4, A5, A6, FINSEQ_1:def 8; :: thesis: verum

end;

given y being object such that A7: y in X and
A8: x = <*y*> ; :: thesis: x in product <*X*>

A9: now :: thesis: for a being object st a in Seg 1 holds
<*y*> . a in <*X*> . a

let a be object ; :: 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:2, TARSKI:def 1;
hence <*y*> . a in <*X*> . a by A7; :: thesis: verum

end;

dom <*y*> = Seg 1 by FINSEQ_1:def 8;
hence x in product <*X*> by A1, A8, A9, CARD_3:def 5; :: thesis: verum