let M be non empty set ; :: thesis: for V being ComplexNormSpace

for f being PartFunc of M,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,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,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 ;

hence (- f) /. x = - (f /. x) by VFUNCT_1:def 5; :: thesis: ||.f.|| . x = ||.(f /. x).||

||.f.|| is total by A1, Th36;

then dom ||.f.|| = M ;

hence ||.f.|| . x = ||.(f /. x).|| by NORMSP_0:def 3; :: thesis: verum

for f being PartFunc of M,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,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,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 ;

hence (- f) /. x = - (f /. x) by VFUNCT_1:def 5; :: thesis: ||.f.|| . x = ||.(f /. x).||

||.f.|| is total by A1, Th36;

then dom ||.f.|| = M ;

hence ||.f.|| . x = ||.(f /. x).|| by NORMSP_0:def 3; :: thesis: verum