let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,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,V
for z being Complex st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}

let f be PartFunc of M,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 :: thesis: for x being Element of M holds
( ( x in (z (#) f) " {(0. V)} implies x in f " {(0. V)} ) & ( x in f " {(0. V)} implies x in (z (#) f) " {(0. V)} ) )
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 A2: x in (z (#) f) " {(0. V)} ; :: thesis: x in f " {(0. V)}
then A3: x in dom (z (#) f) by PARTFUN2:26;
(z (#) f) /. x in {(0. V)} by ;
then (z (#) f) /. x = 0. V by TARSKI:def 1;
then z * (f /. x) = 0. V by ;
then z * (f /. x) = z * (0. V) by CLVECT_1:1;
then f /. x = 0. V by ;
then A4: f /. x in {(0. V)} by TARSKI:def 1;
x in dom f by ;
hence x in f " {(0. V)} by ; :: thesis: verum
end;
assume A5: x in f " {(0. V)} ; :: thesis: x in (z (#) f) " {(0. V)}
then x in dom f by PARTFUN2:26;
then A6: x in dom (z (#) f) by Def2;
f /. x in {(0. V)} by ;
then z * (f /. x) = z * (0. V) by TARSKI:def 1;
then z * (f /. x) = 0. V by CLVECT_1:1;
then (z (#) f) /. x = 0. V by ;
then (z (#) f) /. x in {(0. V)} by TARSKI:def 1;
hence x in (z (#) f) " {(0. V)} by ; :: thesis: verum
end;
hence (z (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; :: thesis: verum