let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,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 ComplexNormSpace; :: thesis: for f1, f2 being PartFunc of M,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 M,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 = M & dom f2 = M ) ;
hence dom (f1 + f2) = M /\ M by VFUNCT_1:def 1
.= M ;
:: according to PARTFUN1:def 2 :: thesis: verum
end;
assume f1 + f2 is total ; :: thesis: ( f1 is total & f2 is total )
then dom (f1 + f2) = M ;
then (dom f1) /\ (dom f2) = M by VFUNCT_1:def 1;
then ( M c= dom f1 & M c= dom f2 ) by XBOOLE_1:17;
hence ( dom f1 = M & dom f2 = M ) ; :: according to PARTFUN1:def 2 :: 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 = M & dom f2 = M ) ;
hence dom (f1 - f2) = M /\ M by VFUNCT_1:def 2
.= M ;
:: according to PARTFUN1:def 2 :: thesis: verum
end;
assume f1 - f2 is total ; :: thesis: ( f1 is total & f2 is total )
then dom (f1 - f2) = M ;
then (dom f1) /\ (dom f2) = M by VFUNCT_1:def 2;
then ( M c= dom f1 & M c= dom f2 ) by XBOOLE_1:17;
hence ( dom f1 = M & dom f2 = M ) ; :: according to PARTFUN1:def 2 :: thesis: verum
end;