let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Complex
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for z being Complex
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let f be PartFunc of M,V; :: thesis: for z being Complex
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let z be Complex; :: thesis: for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
let x be Element of M; :: thesis: ( f is total implies (z (#) f) /. x = z * (f /. x) )
assume f is total ; :: thesis: (z (#) f) /. x = z * (f /. x)
then z (#) f is total by Th34;
then dom (z (#) f) = M ;
hence (z (#) f) /. x = z * (f /. x) by Def2; :: thesis: verum