let C be non empty set ; :: thesis: for V being RealNormSpace
for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let V be RealNormSpace; :: thesis: for f2 being PartFunc of C,the carrier of V
for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f2 be PartFunc of C,the carrier of V; :: thesis: for f1 being PartFunc of C,REAL holds
( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
let f1 be PartFunc of C,REAL ; :: 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 = C & dom f2 = C ) by PARTFUN1:def 4;
hence dom (f1 (#) f2) = C /\ C by Def3
.= C ;
:: according to PARTFUN1:def 4 :: thesis: verum

end;

assume f1 (#) f2 is total ; :: thesis: ( f1 is total & f2 is total )
then dom (f1 (#) f2) = C by PARTFUN1:def 4;
then (dom f1) /\ (dom f2) = C by Def3;
then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def 10; :: according to PARTFUN1:def 4 :: thesis: verum