let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,the carrier of V
for z being Complex holds
( f is total iff z (#) f is total )
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,the carrier of V
for z being Complex holds
( f is total iff z (#) f is total )
let f be PartFunc of M,the carrier of V; :: thesis: for z being Complex holds
( f is total iff z (#) f is total )
let z be Complex; :: thesis: ( f is total iff z (#) f is total )
thus ( f is total implies z (#) f is total ) :: thesis: ( z (#) f is total implies f is total )

proof

assume f is total ; :: thesis: z (#) f is total
then dom f = M by PARTFUN1:def 4;
hence dom (z (#) f) = M by Def4; :: according to PARTFUN1:def 4 :: thesis: verum

end;

assume z (#) f is total ; :: thesis: f is total
then dom (z (#) f) = M by PARTFUN1:def 4;
hence dom f = M by Def4; :: according to PARTFUN1:def 4 :: thesis: verum