let C be non empty set ; :: thesis: for V being RealNormSpace
for f2 being PartFunc of C,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,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,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 ) )
assume f1 (#) f2 is total ; :: thesis: ( f1 is total & f2 is total )
then (dom f1) /\ (dom f2) = C by Def3;
hence ( dom f1 = C & dom f2 = C ) by XBOOLE_1:17; :: according to PARTFUN1:def 2 :: thesis: verum