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 that
A1: f1 is total and
A2: f2 is total ; :: thesis:
A3: dom f2 = C by A2, PARTFUN1:def 2;
dom f1 = C by A1, PARTFUN1:def 2;
hence dom (f1 + f2) = C /\ C by A3, VALUED_1:def 1
.= C ;
:: according to PARTFUN1:def 2 :: thesis:

end;

assume f1 + f2 is total ; :: thesis:
then dom (f1 + f2) = C by PARTFUN1:def 2;
then A4: (dom f1) /\ (dom f2) = C by VALUED_1:def 1;
then A5: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A4, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A5, XBOOLE_0:def 10; :: 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 that
A6: f1 is total and
A7: f2 is total ; :: thesis:
A8: dom f2 = C by A7, PARTFUN1:def 2;
dom f1 = C by A6, PARTFUN1:def 2;
hence dom (f1 - f2) = C /\ C by A8, VALUED_1:12
.= C ;
:: according to PARTFUN1:def 2 :: thesis:

end;

assume f1 - f2 is total ; :: thesis:
then dom (f1 - f2) = C by PARTFUN1:def 2;
then A9: (dom f1) /\ (dom f2) = C by VALUED_1:12;
then A10: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A9, XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) by A10, XBOOLE_0:def 10; :: according to PARTFUN1:def 2 :: thesis:

end;

thus ( f1 is total & f2 is total implies f1 (#) f2 is total ) :: thesis:

assume that
A11: f1 is total and
A12: f2 is total ; :: thesis:
A13: dom f2 = C by A12, PARTFUN1:def 2;
dom f1 = C by A11, PARTFUN1:def 2;
hence dom (f1 (#) f2) = C /\ C by A13, VALUED_1:def 4
.= C ;
:: according to PARTFUN1:def 2 :: thesis:

end;

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