let x, y, X, Y be set ; :: thesis: ( 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 ) ; :: thesis: <%x,y%> in product <%X,Y%>
A2: len <%X,Y%> = 2 by AFINSQ_1:38;
A3: len <%x,y%> = dom <%x,y%> ;
now :: thesis: for a being object st a in dom <%X,Y%> holds
<%x,y%> . a in <%X,Y%> . a
let a be object ; :: thesis: ( a in dom <%X,Y%> implies <%x,y%> . a in <%X,Y%> . a )
assume a in dom <%X,Y%> ; :: thesis: <%x,y%> . a in <%X,Y%> . a
then ( a = 0 or a = 1 ) by A2, TARSKI:def 2, CARD_1:50;
hence <%x,y%> . a in <%X,Y%> . a by A1; :: thesis: verum
end;
hence <%x,y%> in product <%X,Y%> by A2, A3, CARD_3:9, AFINSQ_1:38; :: thesis: verum