let D be non empty set ; for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
let Y be RealNormSpace; for H1, H2 being Functional_Sequence of D, the carrier of Y
for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
let H1, H2 be Functional_Sequence of D, the carrier of Y; for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds
( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
let X be set ; ( H1 is_point_conv_on X & H2 is_point_conv_on X implies ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) ) )
assume that
A1:
H1 is_point_conv_on X
and
A2:
H2 is_point_conv_on X
; ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
thus A8:
H1 + H2 is_point_conv_on X
by A1, A2, A3, Th36, Th19; ( lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
A9:
now for x being Element of D st x in dom ((lim (H1,X)) + (lim (H2,X))) holds
((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + H2) # x)let x be
Element of
D;
( x in dom ((lim (H1,X)) + (lim (H2,X))) implies ((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + H2) # x) )assume A10:
x in dom ((lim (H1,X)) + (lim (H2,X)))
;
((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + H2) # x)then A11:
x in (dom (lim (H1,X))) /\ (dom (lim (H2,X)))
by VFUNCT_1:def 1;
then A12:
x in dom (lim (H2,X))
by XBOOLE_0:def 4;
A13:
x in dom (lim (H1,X))
by A11, XBOOLE_0:def 4;
then A14:
x in X
by A1, Def13;
then A15:
(
H1 # x is
convergent &
H2 # x is
convergent )
by A1, A2, Th19;
X15:
(lim (H1,X)) . x = (lim (H1,X)) /. x
by A13, PARTFUN1:def 6;
X16:
(lim (H2,X)) . x = (lim (H2,X)) /. x
by A12, PARTFUN1:def 6;
thus ((lim (H1,X)) + (lim (H2,X))) . x =
((lim (H1,X)) + (lim (H2,X))) /. x
by A10, PARTFUN1:def 6
.=
((lim (H1,X)) /. x) + ((lim (H2,X)) /. x)
by A10, VFUNCT_1:def 1
.=
(lim (H1 # x)) + ((lim (H2,X)) /. x)
by X15, A1, A13, Def13
.=
(lim (H1 # x)) + (lim (H2 # x))
by X16, A2, A12, Def13
.=
lim ((H1 # x) + (H2 # x))
by A15, NORMSP_1:25
.=
lim ((H1 + H2) # x)
by A1, A2, A14, Th30
;
verum end;
A24:
now for x being Element of D st x in dom ((lim (H1,X)) - (lim (H2,X))) holds
((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - H2) # x)let x be
Element of
D;
( x in dom ((lim (H1,X)) - (lim (H2,X))) implies ((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - H2) # x) )assume A25:
x in dom ((lim (H1,X)) - (lim (H2,X)))
;
((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - H2) # x)then A26:
x in (dom (lim (H1,X))) /\ (dom (lim (H2,X)))
by VFUNCT_1:def 2;
then A27:
x in dom (lim (H2,X))
by XBOOLE_0:def 4;
A28:
x in dom (lim (H1,X))
by A26, XBOOLE_0:def 4;
then A29:
x in X
by A1, Def13;
then A30:
(
H1 # x is
convergent &
H2 # x is
convergent )
by A1, A2, Th19;
X15:
(lim (H1,X)) . x = (lim (H1,X)) /. x
by A28, PARTFUN1:def 6;
X16:
(lim (H2,X)) . x = (lim (H2,X)) /. x
by A27, PARTFUN1:def 6;
thus ((lim (H1,X)) - (lim (H2,X))) . x =
((lim (H1,X)) - (lim (H2,X))) /. x
by A25, PARTFUN1:def 6
.=
((lim (H1,X)) /. x) - ((lim (H2,X)) /. x)
by A25, VFUNCT_1:def 2
.=
(lim (H1 # x)) - ((lim (H2,X)) /. x)
by X15, A1, A28, Def13
.=
(lim (H1 # x)) - (lim (H2 # x))
by X16, A2, A27, Def13
.=
lim ((H1 # x) - (H2 # x))
by A30, NORMSP_1:26
.=
lim ((H1 - H2) # x)
by A1, A2, A29, Th30
;
verum end;
dom ((lim (H1,X)) + (lim (H2,X))) =
(dom (lim (H1,X))) /\ (dom (lim (H2,X)))
by VFUNCT_1:def 1
.=
X /\ (dom (lim (H2,X)))
by A1, Def13
.=
X /\ X
by A2, Def13
.=
X
;
hence
lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X))
by A8, A9, Def13; ( H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) )
X common_on_dom H1 - H2
by A1, A2, Th36;
hence A31:
H1 - H2 is_point_conv_on X
by A5, Th19; lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X))
dom ((lim (H1,X)) - (lim (H2,X))) =
(dom (lim (H1,X))) /\ (dom (lim (H2,X)))
by VFUNCT_1:def 2
.=
X /\ (dom (lim (H2,X)))
by A1, Def13
.=
X /\ X
by A2, Def13
.=
X
;
hence
lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X))
by A31, A24, Def13; verum