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)}

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)} ) )

hence
(z (#) f) " {(0. V)} = f " {(0. V)}
by SUBSET_1:3; :: thesis: verum( ( 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)} )

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;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 A5:
x in f " {(0. V)}
; :: thesis: x in (z (#) f) " {(0. V)}
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;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

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