let x, y, X, Y be set ; ( x in X & y in Y implies <%x,y%> in product <%X,Y%> )
set f = <%X,Y%>;
set g = <%x,y%>;
assume A1:
( x in X & y in Y )
; <%x,y%> in product <%X,Y%>
A2:
len <%X,Y%> = 2
by AFINSQ_1:38;
A3:
len <%x,y%> = dom <%x,y%>
;
now for a being object st a in dom <%X,Y%> holds
<%x,y%> . a in <%X,Y%> . alet a be
object ;
( a in dom <%X,Y%> implies <%x,y%> . a in <%X,Y%> . a )assume
a in dom <%X,Y%>
;
<%x,y%> . a in <%X,Y%> . athen
(
a = 0 or
a = 1 )
by A2, TARSKI:def 2, CARD_1:50;
hence
<%x,y%> . a in <%X,Y%> . a
by A1;
verum end;
hence
<%x,y%> in product <%X,Y%>
by A2, A3, CARD_3:9, AFINSQ_1:38; verum