let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M, the carrier of V
for x being Element of M st f is total holds
( (- f) /. x = - (f /. x) & ||.f.|| . x = ||.(f /. x).|| )
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M, the carrier of V
for x being Element of M st f is total holds
( (- f) /. x = - (f /. x) & ||.f.|| . x = ||.(f /. x).|| )
let f be PartFunc of M, the carrier of V; :: thesis: for x being Element of M st f is total holds
( (- f) /. x = - (f /. x) & ||.f.|| . x = ||.(f /. x).|| )
let x be Element of M; :: thesis: ( f is total implies ( (- f) /. x = - (f /. x) & ||.f.|| . x = ||.(f /. x).|| ) )
assume A1: f is total ; :: thesis: ( (- f) /. x = - (f /. x) & ||.f.|| . x = ||.(f /. x).|| )
then - f is total by Th35;
then dom (- f) = M by PARTFUN1:def 4;
hence (- f) /. x = - (f /. x) by Def6; :: thesis: ||.f.|| . x = ||.(f /. x).||
||.f.|| is total by A1, Th36;
then dom ||.f.|| = M by PARTFUN1:def 4;
hence ||.f.|| . x = ||.(f /. x).|| by NORMSP_0:def 3; :: thesis: verum