let x, y be object ; :: thesis: ( x <> y implies <%x,y%> is one-to-one )
assume A1: x <> y ; :: thesis: <%x,y%> is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom <%x,y%> & x2 in dom <%x,y%> & <%x,y%> . x1 = <%x,y%> . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom <%x,y%> & x2 in dom <%x,y%> & <%x,y%> . x1 = <%x,y%> . x2 implies b₁ = b₂ )
assume A2: ( x1 in dom <%x,y%> & x2 in dom <%x,y%> & <%x,y%> . x1 = <%x,y%> . x2 ) ; :: thesis: b₁ = b₂
then ( x1 in {0,1} & x2 in {0,1} ) by Th7;

per cases then ( ( x1 = 0 & x2 = 0 ) or ( x1 = 0 & x2 = 1 ) or ( x1 = 1 & x2 = 0 ) or ( x1 = 1 & x2 = 1 ) ) by TARSKI:def 2;

suppose ( x1 = 0 & x2 = 0 ) ; :: thesis: b₁ = b₂

hence x1 = x2 ; :: thesis: verum

end;

suppose ( x1 = 0 & x2 = 1 ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A1, A2; :: thesis: verum

end;

suppose ( x1 = 1 & x2 = 0 ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A1, A2; :: thesis: verum

end;

suppose ( x1 = 1 & x2 = 1 ) ; :: thesis: b₁ = b₂

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence <%x,y%> is one-to-one by FUNCT_1:def 4; :: thesis: verum