let C be non empty set ; :: thesis: for V being RealNormSpace
for f1, f2 being PartFunc of C,the carrier of V holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) )
let V be RealNormSpace; :: thesis: for f1, f2 being PartFunc of C,the carrier of V holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) )
let f1, f2 be PartFunc of C,the carrier of V; :: thesis: ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) )
thus ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) :: thesis: ( ( f1 is total & f2 is total ) iff f1 - f2 is total )

proof

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 Def1
.= 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 Def1;
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

end;

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

proof

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 Def2
.= 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 Def2;
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

end;