let C be non empty set ; :: thesis:
let f1, f2 be PartFunc of C,REAL; :: thesis:
thus ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) :: thesis:

thus ( f1 is total & f2 is total implies f1 + f2 is total ) ; :: thesis:
assume f1 + f2 is total ; :: thesis:
then dom (f1 + f2) = C ;
then A1: (dom f1) /\ (dom f2) = C by VALUED_1:def 1;
then A2: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A1, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A2; :: according to PARTFUN1:def 2 :: thesis:

end;

thus ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) :: thesis:

thus ( f1 is total & f2 is total implies f1 - f2 is total ) ; :: thesis:
assume f1 - f2 is total ; :: thesis:
then dom (f1 - f2) = C ;
then A3: (dom f1) /\ (dom f2) = C by VALUED_1:12;
then A4: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A3, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A4; :: according to PARTFUN1:def 2 :: thesis:

end;

thus ( f1 is total & f2 is total implies f1 (#) f2 is total ) ; :: thesis:
assume f1 (#) f2 is total ; :: thesis:
then dom (f1 (#) f2) = C ;
then A5: (dom f1) /\ (dom f2) = C by VALUED_1:def 4;
then A6: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A5, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A6; :: according to PARTFUN1:def 2 :: thesis: