let a, b, x, y, z be set ; :: 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 BVFUNC14:11
.= {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 FUNCT_4:62; :: according to FUNCT_1:def 11 :: thesis: for b₁ being set 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 set ; :: 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 FUNCT_4:89
.= ((a,b) --> (z,y)) . k by A1, A4, FUNCT_4:63 ;
:: 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 FUNCT_4:14
.= y by A1, A5, FUNCT_4:84
.= ((a,b) --> (z,y)) . k by A5, FUNCT_4:63 ; :: thesis: verum

end;

end;