let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Complex
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for z being Complex
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let f be PartFunc of M,V; :: thesis: for z being Complex
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let z be Complex; :: thesis: for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
let Y be set ; :: thesis: ( f | Y is constant implies (z (#) f) | Y is constant )
assume f | Y is constant ; :: thesis: (z (#) f) | Y is constant
then consider r being VECTOR of V such that
A1: for c being Element of M st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;

now :: thesis: for c being Element of M st c in Y /\ (dom (z (#) f)) holds
(z (#) f) /. c = z * r

let c be Element of M; :: thesis: ( c in Y /\ (dom (z (#) f)) implies (z (#) f) /. c = z * r )
assume A2: c in Y /\ (dom (z (#) f)) ; :: thesis: (z (#) f) /. c = z * r
then A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (z (#) f) by A2, XBOOLE_0:def 4;
then c in dom f by Def2;
then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def 4;
thus (z (#) f) /. c = z * (f /. c) by A4, Def2
.= z * r by A1, A5 ; :: thesis: verum

end;

hence (z (#) f) | Y is constant by PARTFUN2:35; :: thesis: verum