let S, T be RealNormSpace; for f1, f2 being PartFunc of S,T
for x0 being Point of S st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
let f1, f2 be PartFunc of S,T; for x0 being Point of S st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
let x0 be Point of S; ( f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) )
assume that
A1:
f1 is_continuous_in x0
and
A2:
f2 is_continuous_in x0
; ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
A3:
( x0 in dom f1 & x0 in dom f2 )
by A1, A2;
now ( x0 in dom (f1 + f2) & ( for s1 being sequence of S st rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) ) )
x0 in (dom f1) /\ (dom f2)
by A3, XBOOLE_0:def 4;
hence A4:
x0 in dom (f1 + f2)
by VFUNCT_1:def 1;
for s1 being sequence of S st rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )let s1 be
sequence of
S;
( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) )assume that A5:
rng s1 c= dom (f1 + f2)
and A6:
(
s1 is
convergent &
lim s1 = x0 )
;
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )A7:
rng s1 c= (dom f1) /\ (dom f2)
by A5, VFUNCT_1:def 1;
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
then
dom (f1 + f2) c= dom f2
by XBOOLE_1:17;
then A8:
rng s1 c= dom f2
by A5;
then A9:
f2 /* s1 is
convergent
by A2, A6;
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
then
dom (f1 + f2) c= dom f1
by XBOOLE_1:17;
then A10:
rng s1 c= dom f1
by A5;
then A11:
f1 /* s1 is
convergent
by A1, A6;
then
(f1 /* s1) + (f2 /* s1) is
convergent
by A9, NORMSP_1:19;
hence
(f1 + f2) /* s1 is
convergent
by A7, Th12;
(f1 + f2) /. x0 = lim ((f1 + f2) /* s1)A12:
f1 /. x0 = lim (f1 /* s1)
by A1, A6, A10;
A13:
f2 /. x0 = lim (f2 /* s1)
by A2, A6, A8;
thus (f1 + f2) /. x0 =
(f1 /. x0) + (f2 /. x0)
by A4, VFUNCT_1:def 1
.=
lim ((f1 /* s1) + (f2 /* s1))
by A11, A12, A9, A13, NORMSP_1:25
.=
lim ((f1 + f2) /* s1)
by A7, Th12
;
verum end;
hence
f1 + f2 is_continuous_in x0
; f1 - f2 is_continuous_in x0
now ( x0 in dom (f1 - f2) & ( for s1 being sequence of S st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) ) )
x0 in (dom f1) /\ (dom f2)
by A3, XBOOLE_0:def 4;
hence A14:
x0 in dom (f1 - f2)
by VFUNCT_1:def 2;
for s1 being sequence of S st rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )let s1 be
sequence of
S;
( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) )assume that A15:
rng s1 c= dom (f1 - f2)
and A16:
(
s1 is
convergent &
lim s1 = x0 )
;
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )A17:
rng s1 c= (dom f1) /\ (dom f2)
by A15, VFUNCT_1:def 2;
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
then
dom (f1 - f2) c= dom f2
by XBOOLE_1:17;
then A18:
rng s1 c= dom f2
by A15;
then A19:
f2 /* s1 is
convergent
by A2, A16;
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
then
dom (f1 - f2) c= dom f1
by XBOOLE_1:17;
then A20:
rng s1 c= dom f1
by A15;
then A21:
f1 /* s1 is
convergent
by A1, A16;
then
(f1 /* s1) - (f2 /* s1) is
convergent
by A19, NORMSP_1:20;
hence
(f1 - f2) /* s1 is
convergent
by A17, Th12;
(f1 - f2) /. x0 = lim ((f1 - f2) /* s1)A22:
f1 /. x0 = lim (f1 /* s1)
by A1, A16, A20;
A23:
f2 /. x0 = lim (f2 /* s1)
by A2, A16, A18;
thus (f1 - f2) /. x0 =
(f1 /. x0) - (f2 /. x0)
by A14, VFUNCT_1:def 2
.=
lim ((f1 /* s1) - (f2 /* s1))
by A21, A22, A19, A23, NORMSP_1:26
.=
lim ((f1 - f2) /* s1)
by A17, Th12
;
verum end;
hence
f1 - f2 is_continuous_in x0
; verum