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, Th29;
A5: ( dom (i .--> d) = {i} & dom (j .--> e) = {j} ) ;
j in dom (f +* (i,d)) by A3, Th29;
hence (f +* (i,d)) +* (j,e) = (f +* (i,d)) +* (j .--> e) by Def2
.= (f +* (i .--> d)) +* (j .--> e) by A2, Def2
.= 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, Def2
.= (f +* (j,e)) +* (i,d) by A4, Def2 ;
:: 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, Th29;
hence (f +* (i,d)) +* (j,e) = f +* (i,d) by Def2
.= (f +* (j,e)) +* (i,d) by A6, Def2 ;
:: 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, Th29;
thus (f +* (i,d)) +* (j,e) = f +* (j,e) by A7, Def2
.= (f +* (j,e)) +* (i,d) by A8, Def2 ; :: 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, Th29;
not j in dom (f +* (i,d)) by A10, Th29;
hence (f +* (i,d)) +* (j,e) = f +* (i,d) by Def2
.= f by A9, Def2
.= f +* (j,e) by A10, Def2
.= (f +* (j,e)) +* (i,d) by A11, Def2 ;
:: thesis: verum

end;

end;