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 b1 being object holds
( not b1 in dom ((a,b,a) --> (x,y,z)) or ((a,b,a) --> (x,y,z)) . b1 = ((a,b) --> (z,y)) . b1 )
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;