let C be non empty set ; :: thesis: for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let c be Element of C; :: thesis: for V being RealNormSpace
for f being PartFunc of C,the carrier of V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let V be RealNormSpace; :: thesis: for f being PartFunc of C,the carrier of V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let f be PartFunc of C,the carrier of V; :: thesis: ( f is total implies ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| ) )
assume A1: f is total ; :: thesis: ( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
then - f is total by Th41;
then dom (- f) = C by PARTFUN1:def 4;
hence (- f) /. c = - (f /. c) by Def6; :: thesis: ||.f.|| . c = ||.(f /. c).||
||.f.|| is total by A1, Th42;
then dom ||.f.|| = C by PARTFUN1:def 4;
hence ||.f.|| . c = ||.(f /. c).|| by Def5; :: thesis: verum