let a, b, c, d be set ; ( a <> b implies ((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c) )
assume A1:
a <> b
; ((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c)
set f = ((a,b) --> (c,d)) * ((a,b) --> (b,a));
A2:
dom ((a,b) --> (b,a)) = {a,b}
by FUNCT_4:62;
b in {a,b}
by TARSKI:def 2;
then A3: (((a,b) --> (c,d)) * ((a,b) --> (b,a))) . b =
((a,b) --> (c,d)) . (((a,b) --> (b,a)) . b)
by A2, FUNCT_1:13
.=
((a,b) --> (c,d)) . a
by FUNCT_4:63
.=
c
by A1, FUNCT_4:63
;
a in {a,b}
by TARSKI:def 2;
then A4: (((a,b) --> (c,d)) * ((a,b) --> (b,a))) . a =
((a,b) --> (c,d)) . (((a,b) --> (b,a)) . a)
by A2, FUNCT_1:13
.=
((a,b) --> (c,d)) . b
by A1, FUNCT_4:63
.=
d
by FUNCT_4:63
;
rng ((a,b) --> (b,a)) =
{a,b}
by A1, FUNCT_4:64
.=
dom ((a,b) --> (c,d))
by FUNCT_4:62
;
hence
((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (a,b) --> (d,c)
by A4, A3, FUNCT_4:66, A2, RELAT_1:27; verum