let a, b, x, y, z be object ; :: thesis: ( a <> b implies (a,b,a) --> (x,y,z) = (a,b) --> (z,y) )
assume A1: a <> b ; :: thesis: (a,b,a) --> (x,y,z) = (a,b) --> (z,y)
A2: dom ((a,b,a) --> (x,y,z)) = {a,b,a} by Th128
.= {a,a,b} by ENUMSET1:57
.= {a,b} by ENUMSET1:30 ;
hence dom ((a,b,a) --> (x,y,z)) = dom ((a,b) --> (z,y)) by Th62; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . b₁ = ((a,b) --> (z,y)) . b₁ )
let k be object ; :: thesis: ( not k in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k )
assume A3: k in dom ((a,b,a) --> (x,y,z)) ; :: thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k

per cases ( k = a or k = b ) by A2, A3, TARSKI:def 2;

suppose A4: k = a ; :: thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k

hence ((a,b,a) --> (x,y,z)) . k = z by Th89
.= ((a,b) --> (z,y)) . k by A1, A4, Th63 ;
:: thesis: verum

end;

suppose A5: k = b ; :: thesis: ((a,b,a) --> (x,y,z)) . k = ((a,b) --> (z,y)) . k

thus ((a,b,a) --> (x,y,z)) . k = ((a .--> x) +* ((b,a) --> (y,z))) . k by Th14
.= y by A1, A5, Th84
.= ((a,b) --> (z,y)) . k by A5, Th63 ; :: thesis: verum

end;

end;