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) /\ (dom (f2 + f3))
by VFUNCT_1:def 2
.=
(dom f1) /\ ((dom f2) /\ (dom f3))
by VFUNCT_1:def 1
.=
((dom f1) /\ (dom f2)) /\ (dom f3)
by XBOOLE_1:16
.=
(dom (f1 - f2)) /\ (dom f3)
by VFUNCT_1:def 2
.=
dom ((f1 - f2) - f3)
by VFUNCT_1:def 2
;
hence
f1 - (f2 + f3) = (f1 - f2) - f3
by A1, PARTFUN2:1; verum