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