let C be non empty set ; :: thesis: for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,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,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,V st f is total holds
( (- f) /. c = - (f /. c) & ||.f.|| . c = ||.(f /. c).|| )
let f be PartFunc of C,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 dom (- f) = C by PARTFUN1:def 2;
hence (- f) /. c = - (f /. c) by Def5; :: thesis: ||.f.|| . c = ||.(f /. c).||
||.f.|| is total by A1, NORMSP_0:def 3;
hence ||.f.|| . c = ||.(f /. c).|| by NORMSP_0:def 3; :: thesis: verum