set X = dom (f1 - f2);
dom (f1 - f2) c= (dom f1) /\ (dom f2) by VALUED_1:12;
then A9: ( dom (f1 - f2) c= dom f1 & dom (f1 - f2) c= dom f2 ) by XBOOLE_1:18;
A10: ( f1 | (dom (f1 - f2)) is continuous & f2 | (dom (f1 - f2)) is continuous ) ;
now :: thesis: for s1 being Real_Sequence st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 in dom (f1 - f2) holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )
let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 in dom (f1 - f2) implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A11: rng s1 c= dom (f1 - f2) and
A12: s1 is convergent and
A13: lim s1 in dom (f1 - f2) ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) )
A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A9, A10, A11, A12, A13, Th13;
then A15: (f1 /* s1) - (f2 /* s1) is convergent ;
A16: rng s1 c= (dom f1) /\ (dom f2) by ;
( f1 . (lim s1) = lim (f1 /* s1) & f2 . (lim s1) = lim (f2 /* s1) ) by A9, A10, A11, A12, A13, Th13;
then (f1 - f2) . (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by
.= lim ((f1 /* s1) - (f2 /* s1)) by
.= lim ((f1 - f2) /* s1) by ;
hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) . (lim s1) = lim ((f1 - f2) /* s1) ) by ; :: thesis: verum
end;
then (f1 - f2) | (dom (f1 - f2)) is continuous by Th13;
hence for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is continuous ; :: thesis: verum