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: i in dom (f +* (j,e)) by A2, Th32;
A5: ( dom (i .--> d) = {i} & dom (j .--> e) = {j} ) by FUNCOP_1:13;
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:14
.= f +* ((j .--> e) +* (i .--> d)) by A1, A5, FUNCT_4:35, ZFMISC_1:11
.= (f +* (j .--> e)) +* (i .--> d) by FUNCT_4:14
.= (f +* (j,e)) +* (i .--> d) by A3, Def3
.= (f +* (j,e)) +* (i,d) by A4, 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;