let z, X, Y be set ; ( 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%>
; 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
; ex y being set st
( f . 0 in X & y in Y & z = <%(f . 0),y%> )
take
f . 1
; ( 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; verum