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 holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let V be ComplexNormSpace; :: thesis: for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f2 be PartFunc of M,V; :: thesis: for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f1 be PartFunc of M,COMPLEX; :: thesis: ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
thus ( f1 is total & f2 is total implies f1 (#) f2 is total ) :: thesis: ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) )

proof

assume ( f1 is total & f2 is total ) ; :: thesis: f1 (#) f2 is total
then ( dom f1 = M & dom f2 = M ) ;
hence dom (f1 (#) f2) = M /\ M by Def1
.= M ;
:: according to PARTFUN1:def 2 :: thesis: verum

end;

assume f1 (#) f2 is total ; :: thesis: ( f1 is total & f2 is total )
then dom (f1 (#) f2) = M ;
then (dom f1) /\ (dom f2) = M by Def1;
then ( M c= dom f1 & M c= dom f2 ) by XBOOLE_1:17;
hence ( dom f1 = M & dom f2 = M ) ; :: according to PARTFUN1:def 2 :: thesis: verum