let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z1, z2 being Complex holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for z1, z2 being Complex holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
let f be PartFunc of M,V; :: thesis: for z1, z2 being Complex holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
let z1, z2 be Complex; :: thesis: (z1 * z2) (#) f = z1 (#) (z2 (#) f)
A1: dom ((z1 * z2) (#) f) = dom f by Def2
.= dom (z2 (#) f) by Def2
.= dom (z1 (#) (z2 (#) f)) by Def2 ;

now :: thesis: for x being Element of M st x in dom ((z1 * z2) (#) f) holds
((z1 * z2) (#) f) /. x = (z1 (#) (z2 (#) f)) /. x

let x be Element of M; :: thesis: ( x in dom ((z1 * z2) (#) f) implies ((z1 * z2) (#) f) /. x = (z1 (#) (z2 (#) f)) /. x )
assume A2: x in dom ((z1 * z2) (#) f) ; :: thesis: ((z1 * z2) (#) f) /. x = (z1 (#) (z2 (#) f)) /. x
then A3: x in dom (z2 (#) f) by A1, Def2;
thus ((z1 * z2) (#) f) /. x = (z1 * z2) * (f /. x) by A2, Def2
.= z1 * (z2 * (f /. x)) by CLVECT_1:def 4
.= z1 * ((z2 (#) f) /. x) by A3, Def2
.= (z1 (#) (z2 (#) f)) /. x by A1, A2, Def2 ; :: thesis: verum

end;

hence (z1 * z2) (#) f = z1 (#) (z2 (#) f) by A1, PARTFUN2:1; :: thesis: verum