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 A2, PARTFUN2:26;
then (z (#) f) /. x = 0. V by TARSKI:def 1;
then z * (f /. x) = 0. V by A3, Def2;
then z * (f /. x) = z * (0. V) by CLVECT_1:1;
then f /. x = 0. V by A1, CLVECT_1:11;
then A4: f /. x in {(0. V)} by TARSKI:def 1;
x in dom f by A3, Def2;
hence x in f " {(0. V)} by A4, PARTFUN2:26; :: 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 A5, PARTFUN2:26;
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 A6, Def2;
then (z (#) f) /. x in {(0. V)} by TARSKI:def 1;
hence x in (z (#) f) " {(0. V)} by A6, PARTFUN2:26; :: thesis: verum
end;
hence (z (#) f) " {(0. V)} = f " {(0. V)} by SUBSET_1:3; :: thesis: verum