let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let V be ComplexNormSpace; :: thesis: for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let f2 be PartFunc of M,V; :: thesis: for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let f1 be PartFunc of M,COMPLEX; :: thesis: for x being Element of M st f1 is total & f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
let x be Element of M; :: thesis: ( f1 is total & f2 is total implies (f1 (#) f2) /. x = (f1 /. x) * (f2 /. x) )
assume ( f1 is total & f2 is total ) ; :: thesis: (f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
then f1 (#) f2 is total by Th33;
then dom (f1 (#) f2) = M ;
hence (f1 (#) f2) /. x = (f1 /. x) * (f2 /. x) by Def1; :: thesis: verum