let x, y be set ; :: thesis: <%x,y%> = (0,1) --> (x,y)
A: dom <%x,y%> = len <%x,y%>
.= {0,1} by Th42, CARD_1:88 ;
B: <%x,y%> . 0 = x by Th42;
<%x,y%> . 1 = y by Th42;
hence <%x,y%> = (0,1) --> (x,y) by A, B, FUNCT_4:69; :: thesis: verum