let C be non empty set ; :: thesis:
let f1, f2 be PartFunc of C,COMPLEX; :: 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 is total & f2 is total ) ; :: thesis:
then ( dom f1 = C & dom f2 = C ) ;
hence dom (f1 + f2) = C /\ C by VALUED_1:def 1
.= C ;
:: according to PARTFUN1:def 2 :: thesis:

end;

assume f1 + f2 is total ; :: thesis:
then dom (f1 + f2) = C ;
then (dom f1) /\ (dom f2) = C by VALUED_1:def 1;
then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) ; :: 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 is total & f2 is total ) ; :: thesis:
then ( dom f1 = C & dom f2 = C ) ;
hence dom (f1 - f2) = C /\ C by Th2
.= C ;
:: according to PARTFUN1:def 2 :: thesis:

end;

assume f1 - f2 is total ; :: thesis:
then dom (f1 - f2) = C ;
then (dom f1) /\ (dom f2) = C by Th2;
then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence ( dom f1 = C & dom f2 = C ) ; :: according to PARTFUN1:def 2 :: thesis:

end;

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

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

end;

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