let f be Function; :: thesis: for d, e, i, j being set st i <> j holds
(f +* i,d) +* j,e = (f +* j,e) +* i,d
let d, e, i, j be set ; :: thesis: ( i <> j implies (f +* i,d) +* j,e = (f +* j,e) +* i,d )
assume A1: i <> j ; :: thesis: (f +* i,d) +* j,e = (f +* j,e) +* i,d

per cases ( ( i in dom f & j in dom f ) or ( i in dom f & not j in dom f ) or ( not i in dom f & j in dom f ) or ( not i in dom f & not j in dom f ) ) ;

suppose that A2: i in dom f and
A3: j in dom f ; :: thesis: (f +* i,d) +* j,e = (f +* j,e) +* i,d

A4: ( dom (i .--> d) = {i} & dom (j .--> e) = {j} ) by FUNCOP_1:19;
A5: i in dom (f +* j,e) by A2, Th32;
j in dom (f +* i,d) by A3, Th32;
hence (f +* i,d) +* j,e = (f +* i,d) +* (j .--> e) by Def3
.= (f +* (i .--> d)) +* (j .--> e) by A2, Def3
.= f +* ((i .--> d) +* (j .--> e)) by FUNCT_4:15
.= f +* ((j .--> e) +* (i .--> d)) by A1, A4, FUNCT_4:36, ZFMISC_1:17
.= (f +* (j .--> e)) +* (i .--> d) by FUNCT_4:15
.= (f +* j,e) +* (i .--> d) by A3, Def3
.= (f +* j,e) +* i,d by A5, Def3 ;
:: thesis: verum

end;

suppose that i in dom f and
A6: not j in dom f ; :: thesis: (f +* i,d) +* j,e = (f +* j,e) +* i,d

not j in dom (f +* i,d) by A6, Th32;
hence (f +* i,d) +* j,e = f +* i,d by Def3
.= (f +* j,e) +* i,d by A6, Def3 ;
:: thesis: verum

end;

suppose that A7: not i in dom f and
j in dom f ; :: thesis: (f +* i,d) +* j,e = (f +* j,e) +* i,d

A8: not i in dom (f +* j,e) by A7, Th32;
thus (f +* i,d) +* j,e = f +* j,e by A7, Def3
.= (f +* j,e) +* i,d by A8, Def3 ; :: thesis: verum

end;

suppose that A9: not i in dom f and
A10: not j in dom f ; :: thesis: (f +* i,d) +* j,e = (f +* j,e) +* i,d

A11: not i in dom (f +* j,e) by A9, Th32;
not j in dom (f +* i,d) by A10, Th32;
hence (f +* i,d) +* j,e = f +* i,d by Def3
.= f by A9, Def3
.= f +* j,e by A10, Def3
.= (f +* j,e) +* i,d by A11, Def3 ;
:: thesis: verum

end;

end;