let CNS1, CNS2 be ComplexNormSpace; :: thesis: for h being PartFunc of CNS1,CNS2
for seq being sequence of CNS1
for z being Complex st rng seq c= dom h holds
(z (#) h) /* seq = z * (h /* seq)
let h be PartFunc of CNS1,CNS2; :: thesis: for seq being sequence of CNS1
for z being Complex st rng seq c= dom h holds
(z (#) h) /* seq = z * (h /* seq)
let seq be sequence of CNS1; :: thesis: for z being Complex st rng seq c= dom h holds
(z (#) h) /* seq = z * (h /* seq)
let z be Complex; :: thesis: ( rng seq c= dom h implies (z (#) h) /* seq = z * (h /* seq) )
assume A1: rng seq c= dom h ; :: thesis: (z (#) h) /* seq = z * (h /* seq)
then A2: rng seq c= dom (z (#) h) by VFUNCT_2:def 2;

now :: thesis: for n being Nat holds ((z (#) h) /* seq) . n = z * ((h /* seq) . n)

let n be Nat; :: thesis: ((z (#) h) /* seq) . n = z * ((h /* seq) . n)
A3: n in NAT by ORDINAL1:def 12;
A4: seq . n in dom (z (#) h) by A2, Th4;
thus ((z (#) h) /* seq) . n = (z (#) h) /. (seq . n) by A2, FUNCT_2:109, A3
.= z * (h /. (seq . n)) by A4, VFUNCT_2:def 2
.= z * ((h /* seq) . n) by A1, FUNCT_2:109, A3 ; :: thesis: verum

end;

hence (z (#) h) /* seq = z * (h /* seq) by CLVECT_1:def 14; :: thesis: verum