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

now :: thesis: for c being Element of M holds
( ( c in ||.f.|| " {0} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in ||.f.|| " {0} ) )

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 7;
||.f.|| . c in {0} by A1, FUNCT_1:def 7;
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:26; :: thesis: verum

end;

assume A4: c in f " {(0. V)} ; :: thesis: c in ||.f.|| " {0}
then c in dom f by PARTFUN2:26;
then A5: c in dom ||.f.|| by NORMSP_0:def 3;
f /. c in {(0. V)} by A4, PARTFUN2:26;
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 7; :: thesis: verum

end;

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

now :: thesis: for c being Element of M holds
( ( c in (- f) " {(0. V)} implies c in f " {(0. V)} ) & ( c in f " {(0. V)} implies c in (- f) " {(0. V)} ) )

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:26;
(- f) /. c in {(0. V)} by A6, PARTFUN2:26;
then (- f) /. c = 0. V by TARSKI:def 1;
then - (- (f /. c)) = - (0. V) by A7, VFUNCT_1:def 5;
then - (- (f /. c)) = 0. V by RLVECT_1:12;
then f /. c = 0. V by RLVECT_1:17;
then A8: f /. c in {(0. V)} by TARSKI:def 1;
c in dom f by A7, VFUNCT_1:def 5;
hence c in f " {(0. V)} by A8, PARTFUN2:26; :: thesis: verum

end;

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

end;

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