let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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)) )
A3: now :: thesis: for x being Element of D st x in X holds
(H1 + H2) # x is convergent
let x be Element of D; :: thesis: ( x in X implies (H1 + H2) # x is convergent )
assume A4: x in X ; :: thesis: (H1 + H2) # x is convergent
then ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th19;
then (H1 # x) + (H2 # x) is convergent by NORMSP_1:19;
hence (H1 + H2) # x is convergent by A1, A2, A4, Th30; :: thesis: verum
end;
A5: now :: thesis: for x being Element of D st x in X holds
(H1 - H2) # x is convergent
let x be Element of D; :: thesis: ( x in X implies (H1 - H2) # x is convergent )
assume A6: x in X ; :: thesis: (H1 - H2) # x is convergent
then ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th19;
then (H1 # x) - (H2 # x) is convergent by NORMSP_1:20;
hence (H1 - H2) # x is convergent by A1, A2, A6, Th30; :: thesis: verum
end;
thus A8: H1 + H2 is_point_conv_on X by A1, A2, A3, Th36, Th19; :: thesis: ( 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 :: thesis: 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; :: thesis: ( 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))) ; :: thesis: ((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 ; :: thesis: verum
end;
A24: now :: thesis: 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; :: thesis: ( 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))) ; :: thesis: ((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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum