let z, X, Y be set ; :: thesis: ( z in product <%X,Y%> implies ex x, y being set st
( x in X & y in Y & z = <%x,y%> ) )
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
A1: z = f and
A2: dom f = dom <%X,Y%> and
A3: 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 XFinSequence by A2, AFINSQ_1:5;
take f . 0 ; :: thesis: ex y being set st
( f . 0 in X & y in Y & z = <%(f . 0),y%> )
take f . 1 ; :: thesis: ( f . 0 in X & f . 1 in Y & z = <%(f . 0),(f . 1)%> )
A4: ( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def 2;
A5: ( <%X,Y%> . 0 = X & <%X,Y%> . 1 = Y ) ;
len <%X,Y%> = 2 by AFINSQ_1:38;
then len f = 2 by A2;
hence ( f . 0 in X & f . 1 in Y & z = <%(f . 0),(f . 1)%> ) by A5, A4, A1, A2, A3, AFINSQ_1:38, CARD_1:50; :: thesis: verum