let M be non empty set ; for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Complex
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let V be ComplexNormSpace; for f2 being PartFunc of M,V
for z being Complex
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let f2 be PartFunc of M,V; for z being Complex
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let z be Complex; for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
let f1 be PartFunc of M,COMPLEX; z (#) (f1 (#) f2) = (z (#) f1) (#) f2
A1:
dom (f1 (#) f2) = (dom f1) /\ (dom f2)
by Def1;
A2: dom (z (#) (f1 (#) f2)) =
dom (f1 (#) f2)
by Def2
.=
(dom (z (#) f1)) /\ (dom f2)
by A1, VALUED_1:def 5
.=
dom ((z (#) f1) (#) f2)
by Def1
;
hence
z (#) (f1 (#) f2) = (z (#) f1) (#) f2
by A2, PARTFUN2:1; verum