let S be RealNormSpace; for X being set
for f1, f2 being PartFunc of REAL, the carrier of S st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
let X be set ; for f1, f2 being PartFunc of REAL, the carrier of S st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
let f1, f2 be PartFunc of REAL, the carrier of S; ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) )
assume that
A1:
X c= (dom f1) /\ (dom f2)
and
A2:
( f1 | X is continuous & f2 | X is continuous )
; ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
A3:
( X c= dom f1 & X c= dom f2 )
by A1, XBOOLE_1:18;
A4:
( X c= dom (f1 + f2) & X c= dom (f1 - f2) )
by A1, VFUNCT_1:def 1, VFUNCT_1:def 2;
now for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )let s1 be
Real_Sequence;
( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) )assume that A5:
(
rng s1 c= X &
s1 is
convergent )
and A6:
lim s1 in X
;
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )A7:
(
f1 /* s1 is
convergent &
f2 /* s1 is
convergent )
by A3, A2, A5, A6, Th16;
then A8:
(f1 /* s1) + (f2 /* s1) is
convergent
by NORMSP_1:19;
A9:
rng s1 c= (dom f1) /\ (dom f2)
by A1, A5, XBOOLE_1:1;
A10:
lim s1 in REAL
by XREAL_0:def 1;
(
f1 /. (lim s1) = lim (f1 /* s1) &
f2 /. (lim s1) = lim (f2 /* s1) )
by A3, A2, A5, A6, Th16;
then (f1 + f2) /. (lim s1) =
(lim (f1 /* s1)) + (lim (f2 /* s1))
by A4, A6, VFUNCT_1:def 1, A10
.=
lim ((f1 /* s1) + (f2 /* s1))
by A7, NORMSP_1:25
.=
lim ((f1 + f2) /* s1)
by A9, Th2
;
hence
(
(f1 + f2) /* s1 is
convergent &
(f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
by A9, A8, Th2;
verum end;
hence
(f1 + f2) | X is continuous
by A4, Th16; (f1 - f2) | X is continuous
now for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )let s1 be
Real_Sequence;
( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) )assume that A11:
(
rng s1 c= X &
s1 is
convergent )
and A12:
lim s1 in X
;
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )A13:
(
f1 /* s1 is
convergent &
f2 /* s1 is
convergent )
by A3, A2, A11, A12, Th16;
then A14:
(f1 /* s1) - (f2 /* s1) is
convergent
by NORMSP_1:20;
A15:
rng s1 c= (dom f1) /\ (dom f2)
by A1, A11, XBOOLE_1:1;
A16:
lim s1 in REAL
by XREAL_0:def 1;
(
f1 /. (lim s1) = lim (f1 /* s1) &
f2 /. (lim s1) = lim (f2 /* s1) )
by A3, A2, A11, A12, Th16;
then (f1 - f2) /. (lim s1) =
(lim (f1 /* s1)) - (lim (f2 /* s1))
by A4, A12, VFUNCT_1:def 2, A16
.=
lim ((f1 /* s1) - (f2 /* s1))
by A13, NORMSP_1:26
.=
lim ((f1 - f2) /* s1)
by A15, Th2
;
hence
(
(f1 - f2) /* s1 is
convergent &
(f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
by A15, A14, Th2;
verum end;
hence
(f1 - f2) | X is continuous
by A4, Th16; verum