let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M, the carrier of V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M, the carrier of V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let f be PartFunc of M, the carrier of V; :: thesis: ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )

now

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

proof

assume A1: c in ||.f.|| " {0} ; :: thesis: c in f " {(0. V)}
then A2: c in dom ||.f.|| by FUNCT_1:def 13;
||.f.|| . c in {0} by A1, FUNCT_1:def 13;
then ||.f.|| . c = 0 by TARSKI:def 1;
then ||.(f /. c).|| = 0 by A2, NORMSP_0:def 3;
then f /. c = 0. V by NORMSP_0:def 5;
then A3: f /. c in {(0. V)} by TARSKI:def 1;
c in dom f by A2, NORMSP_0:def 3;
hence c in f " {(0. V)} by A3, PARTFUN2:44; :: thesis: verum

end;

assume A4: c in f " {(0. V)} ; :: thesis: c in ||.f.|| " {0}
then c in dom f by PARTFUN2:44;
then A5: c in dom ||.f.|| by NORMSP_0:def 3;
f /. c in {(0. V)} by A4, PARTFUN2:44;
then f /. c = 0. V by TARSKI:def 1;
then ||.(f /. c).|| = 0 by NORMSP_0:def 6;
then ||.f.|| . c = 0 by A5, NORMSP_0:def 3;
then ||.f.|| . c in {0} by TARSKI:def 1;
hence c in ||.f.|| " {0} by A5, FUNCT_1:def 13; :: thesis: verum

end;

hence ||.f.|| " {0} = f " {(0. V)} by SUBSET_1:8; :: thesis: (- f) " {(0. V)} = f " {(0. V)}

now

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

proof

assume A6: c in (- f) " {(0. V)} ; :: thesis: c in f " {(0. V)}
then A7: c in dom (- f) by PARTFUN2:44;
(- f) /. c in {(0. V)} by A6, PARTFUN2:44;
then (- f) /. c = 0. V by TARSKI:def 1;
then - (- (f /. c)) = - (0. V) by A7, Def6;
then - (- (f /. c)) = 0. V by RLVECT_1:25;
then f /. c = 0. V by RLVECT_1:30;
then A8: f /. c in {(0. V)} by TARSKI:def 1;
c in dom f by A7, Def6;
hence c in f " {(0. V)} by A8, PARTFUN2:44; :: thesis: verum

end;

assume A9: c in f " {(0. V)} ; :: thesis: c in (- f) " {(0. V)}
then c in dom f by PARTFUN2:44;
then A10: c in dom (- f) by Def6;
f /. c in {(0. V)} by A9, PARTFUN2:44;
then f /. c = 0. V by TARSKI:def 1;
then (- f) /. c = - (0. V) by A10, Def6;
then (- f) /. c = 0. V by RLVECT_1:25;
then (- f) /. c in {(0. V)} by TARSKI:def 1;
hence c in (- f) " {(0. V)} by A10, PARTFUN2:44; :: thesis: verum

end;

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