let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,the carrier of V
for z being Complex st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,the carrier of V
for z being Complex st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
let f be PartFunc of M,the carrier of V; :: thesis: for z being Complex st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
let z be Complex; :: thesis: ( z <> 0c implies (z (#) f) " {(0. V)} = f " {(0. V)} )
assume A1: z <> 0c ; :: thesis: (z (#) f) " {(0. V)} = f " {(0. V)}

now

let x be Element of M; :: thesis: ( ( x in (z (#) f) " {(0. V)} implies x in f " {(0. V)} ) & ( x in f " {(0. V)} implies x in (z (#) f) " {(0. V)} ) )
thus ( x in (z (#) f) " {(0. V)} implies x in f " {(0. V)} ) :: thesis: ( x in f " {(0. V)} implies x in (z (#) f) " {(0. V)} )

proof

assume x in (z (#) f) " {(0. V)} ; :: thesis: x in f " {(0. V)}
then ( x in dom (z (#) f) & (z (#) f) /. x in {(0. V)} ) by PARTFUN2:44;
then ( x in dom (z (#) f) & (z (#) f) /. x = 0. V ) by TARSKI:def 1;
then ( x in dom f & z * (f /. x) = 0. V ) by Def4;
then ( x in dom f & z * (f /. x) = z * (0. V) ) by CLVECT_1:2;
then ( x in dom f & f /. x = 0. V ) by A1, CLVECT_1:12;
then ( x in dom f & f /. x in {(0. V)} ) by TARSKI:def 1;
hence x in f " {(0. V)} by PARTFUN2:44; :: thesis: verum

end;

assume x in f " {(0. V)} ; :: thesis: x in (z (#) f) " {(0. V)}
then ( x in dom f & f /. x in {(0. V)} ) by PARTFUN2:44;
then ( x in dom (z (#) f) & z * (f /. x) = z * (0. V) ) by Def4, TARSKI:def 1;
then ( x in dom (z (#) f) & z * (f /. x) = 0. V ) by CLVECT_1:2;
then ( x in dom (z (#) f) & (z (#) f) /. x = 0. V ) by Def4;
then ( x in dom (z (#) f) & (z (#) f) /. x in {(0. V)} ) by TARSKI:def 1;
hence x in (z (#) f) " {(0. V)} by PARTFUN2:44; :: thesis: verum

end;

hence (z (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:8; :: thesis: verum