let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
let f be PartFunc of C,V; :: thesis: ( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
now :: thesis: for c being Element of C 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 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 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 ;
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 C 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 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 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, Def5;
then f /. c = 0. V ;
then A8: f /. c in {(0. V)} by TARSKI:def 1;
c in dom f by A7, Def5;
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 Def5;
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, Def5;
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