set X = dom (f1 - f2);
dom (f1 - f2) c= (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
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 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;
( 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)
;
( (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, Th16;
then A15:
(f1 /* s1) - (f2 /* s1) is
convergent
by NORMSP_1:20;
A16:
rng s1 c= (dom f1) /\ (dom f2)
by A11, VFUNCT_1:def 2;
(
f1 /. (lim s1) = lim (f1 /* s1) &
f2 /. (lim s1) = lim (f2 /* s1) )
by A9, A10, A11, A12, A13, Th16;
then (f1 - f2) /. (lim s1) =
(lim (f1 /* s1)) - (lim (f2 /* s1))
by A13, VFUNCT_1:def 2
.=
lim ((f1 /* s1) - (f2 /* s1))
by A14, NORMSP_1:26
.=
lim ((f1 - f2) /* s1)
by A16, Th2
;
hence
(
(f1 - f2) /* s1 is
convergent &
(f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
by A16, A15, Th2;
verum end;
then
(f1 - f2) | (dom (f1 - f2)) is continuous
by Th16;
hence
for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is continuous
; verum