let x, y be set ; :: thesis: <%x,y%> = (0,1) --> (x,y)
A1: dom <%x,y%> = len <%x,y%>
.= {0,1} by Th42, CARD_1:50 ;
A2: <%x,y%> . 0 = x by Th42;
<%x,y%> . 1 = y by Th42;
hence <%x,y%> = (0,1) --> (x,y) by A1, A2, FUNCT_4:66; :: thesis: verum