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