let a, b, c, d be set ; :: thesis: ( a <> b implies (a,b --> c,d) * (a,b --> b,a) = a,b --> d,c )
assume A1: a <> b ; :: thesis: (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:65;
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:23
.= (a,b --> c,d) . a by FUNCT_4:66
.= c by A1, FUNCT_4:66 ;
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:23
.= (a,b --> c,d) . b by A1, FUNCT_4:66
.= d by FUNCT_4:66 ;
rng (a,b --> b,a) = {a,b} by A1, FUNCT_4:67
.= dom (a,b --> c,d) by FUNCT_4:65 ;
then dom ((a,b --> c,d) * (a,b --> b,a)) = {a,b} by A2, RELAT_1:46;
hence (a,b --> c,d) * (a,b --> b,a) = a,b --> d,c by A4, A3, FUNCT_4:69; :: thesis: verum