let M be non empty set ; for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
let V be ComplexNormSpace; for f1, f2, f3 being PartFunc of M,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
let f1, f2, f3 be PartFunc of M,V; (f1 + f2) + f3 = f1 + (f2 + f3)
A1: dom ((f1 + f2) + f3) =
(dom (f1 + f2)) /\ (dom f3)
by VFUNCT_1:def 1
.=
((dom f1) /\ (dom f2)) /\ (dom f3)
by VFUNCT_1:def 1
.=
(dom f1) /\ ((dom f2) /\ (dom f3))
by XBOOLE_1:16
.=
(dom f1) /\ (dom (f2 + f3))
by VFUNCT_1:def 1
.=
dom (f1 + (f2 + f3))
by VFUNCT_1:def 1
;
hence
(f1 + f2) + f3 = f1 + (f2 + f3)
by A1, PARTFUN2:1; verum