let f be Function; 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 ; ( i <> j implies (f +* (i,d)) +* (j,e) = (f +* (j,e)) +* (i,d) )
assume A1:
i <> j
; (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
;
(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
;
verum end; suppose that A9:
not
i in dom f
and A10:
not
j in dom f
;
(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
;
verum end; end;