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 + f2) = (f3 (#) f1) + (f3 (#) f2)
let V be ComplexNormSpace; for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let f1, f2 be PartFunc of M,V; for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
let f3 be PartFunc of M,COMPLEX; f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
A1: dom (f3 (#) (f1 + f2)) =
(dom f3) /\ (dom (f1 + f2))
by Def1
.=
(dom f3) /\ ((dom f1) /\ (dom f2))
by VFUNCT_1:def 1
.=
(((dom f3) /\ (dom f3)) /\ (dom f1)) /\ (dom f2)
by XBOOLE_1:16
.=
(((dom f3) /\ (dom f1)) /\ (dom f3)) /\ (dom f2)
by XBOOLE_1:16
.=
((dom f3) /\ (dom f1)) /\ ((dom f3) /\ (dom f2))
by XBOOLE_1:16
.=
(dom (f3 (#) f1)) /\ ((dom f3) /\ (dom f2))
by Def1
.=
(dom (f3 (#) f1)) /\ (dom (f3 (#) f2))
by Def1
.=
dom ((f3 (#) f1) + (f3 (#) f2))
by VFUNCT_1:def 1
;
hence
f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
by A1, PARTFUN2:1; verum