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

now

let c be Element of C; :: 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 c in ||.f.|| " {0 } ; :: thesis: c in f " {(0. V)}
then ( c in dom ||.f.|| & ||.f.|| . c in {0 } ) by FUNCT_1:def 13;
then ( c in dom ||.f.|| & ||.f.|| . c = 0 ) by TARSKI:def 1;
then ( c in dom ||.f.|| & ||.(f /. c).|| = 0 ) by Def5;
then ( c in dom f & f /. c = 0. V ) by Def5, NORMSP_1:def 2;
then ( c in dom f & f /. c in {(0. V)} ) by TARSKI:def 1;
hence c in f " {(0. V)} by PARTFUN2:44; :: thesis: verum

end;

assume c in f " {(0. V)} ; :: thesis: c in ||.f.|| " {0 }
then ( c in dom f & f /. c in {(0. V)} ) by PARTFUN2:44;
then ( c in dom ||.f.|| & f /. c = 0. V ) by Def5, TARSKI:def 1;
then ( c in dom ||.f.|| & ||.(f /. c).|| = 0 ) by NORMSP_1:def 2;
then ( c in dom ||.f.|| & ||.f.|| . c = 0 ) by Def5;
then ( c in dom ||.f.|| & ||.f.|| . c in {0 } ) by TARSKI:def 1;
hence c in ||.f.|| " {0 } by 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 C; :: 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 c in (- f) " {(0. V)} ; :: thesis: c in f " {(0. V)}
then ( c in dom (- f) & (- f) /. c in {(0. V)} ) by PARTFUN2:44;
then ( c in dom (- f) & (- f) /. c = 0. V ) by TARSKI:def 1;
then ( c in dom (- f) & - (- (f /. c)) = - (0. V) ) by Def6;
then ( c in dom (- f) & - (- (f /. c)) = 0. V ) by RLVECT_1:25;
then ( c in dom f & f /. c = 0. V ) by Def6, RLVECT_1:30;
then ( c in dom f & f /. c in {(0. V)} ) by TARSKI:def 1;
hence c in f " {(0. V)} by PARTFUN2:44; :: thesis: verum

end;

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

end;

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