let a, b, c, d be object ; :: thesis: ( a <> b implies (a,b) --> (c,d) = (b,a) --> (d,c) )
assume A1: a <> b ; :: thesis: (a,b) --> (c,d) = (b,a) --> (d,c)
A2: dom ((a,b) --> (c,d)) = {a,b} by FUNCT_4:62;
then A3: dom ((a,b) --> (c,d)) = dom ((b,a) --> (d,c)) by FUNCT_4:62;
for x being object st x in dom ((a,b) --> (c,d)) holds
((a,b) --> (c,d)) . x = ((b,a) --> (d,c)) . x
proof
let x be object ; :: thesis: ( x in dom ((a,b) --> (c,d)) implies ((a,b) --> (c,d)) . x = ((b,a) --> (d,c)) . x )
assume x in dom ((a,b) --> (c,d)) ; :: thesis: ((a,b) --> (c,d)) . x = ((b,a) --> (d,c)) . x
per cases then ( x = a or x = b ) by A2, TARSKI:def 2;
suppose A4: x = a ; :: thesis: ((a,b) --> (c,d)) . x = ((b,a) --> (d,c)) . x
hence ((a,b) --> (c,d)) . x = c by A1, FUNCT_4:63
.= ((b,a) --> (d,c)) . x by A4, FUNCT_4:63 ;
:: thesis: verum
end;
suppose A5: x = b ; :: thesis: ((a,b) --> (c,d)) . x = ((b,a) --> (d,c)) . x
hence ((a,b) --> (c,d)) . x = d by FUNCT_4:63
.= ((b,a) --> (d,c)) . x by A1, A5, FUNCT_4:63 ;
:: thesis: verum
end;
end;
end;
hence (a,b) --> (c,d) = (b,a) --> (d,c) by A3, FUNCT_1:2; :: thesis: verum