let a, X, Y, Z be set ; :: thesis: ( a in product <*X,Y,Z*> iff ex x, y, z being set st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) )
len <*X,Y,Z*> = 3 by FINSEQ_1:62;
then A1: ( dom <*X,Y,Z*> = Seg 3 & 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 & <*X,Y,Z*> . 1 = X & <*X,Y,Z*> . 2 = Y & <*X,Y,Z*> . 3 = Z ) by ENUMSET1:def 1, FINSEQ_1:62, FINSEQ_1:def 3, FINSEQ_3:1;
thus ( a in product <*X,Y,Z*> implies ex x, y, z being set st
( x in X & y in Y & z in Z & a = <*x,y,z*> ) ) :: thesis: ( ex x, y, z being set 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 set st
( x in X & y in Y & z in Z & a = <*x,y,z*> )
then consider f being Function such that
A2: ( a = f & dom f = dom <*X,Y,Z*> & ( for x being set 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 A1, A2, FINSEQ_1:def 2;
take f . 1 ; :: thesis: ex y, z being set st
( f . 1 in X & y in Y & z in Z & a = <*(f . 1),y,z*> )
take f . 2 ; :: thesis: ex z being set 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 A1, A2, 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 A1, A2, FINSEQ_1:62; :: thesis: verum

end;

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

now

let a be set ; :: 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 ENUMSET1:def 1, FINSEQ_3:1;
hence <*x,y,z*> . a in <*X,Y,Z*> . a by A1, A3, FINSEQ_1:62; :: thesis: verum

end;

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