let D be non empty set ; :: thesis: for H1, H2 being Functional_Sequence of D,REAL
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)) & 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,REAL; :: 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)) & 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)) & 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)) & 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 SEQ_2:5;
hence (H1 + H2) # x is convergent by A1, A2, A4, Th33; :: 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 SEQ_2:11;
hence (H1 - H2) # x is convergent by A1, A2, A6, Th33; :: thesis: verum
end;
A7: ( X common_on_dom H1 & X common_on_dom H2 ) by A1, A2;
then X common_on_dom H1 + H2 by Th36;
hence A8: H1 + H2 is_point_conv_on X by A3, 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)) & 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 VALUED_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;
thus ((lim (H1,X)) + (lim (H2,X))) . x = ((lim (H1,X)) . x) + ((lim (H2,X)) . x) by A10, VALUED_1:def 1
.= (lim (H1 # x)) + ((lim (H2,X)) . x) by A1, A13, Def13
.= (lim (H1 # x)) + (lim (H2 # x)) by A2, A12, Def13
.= lim ((H1 # x) + (H2 # x)) by A15, SEQ_2:6
.= lim ((H1 + H2) # x) by A1, A2, A14, Th33 ; :: thesis: verum
end;
A16: 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 A17: 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 SEQ_2:14;
hence (H1 (#) H2) # x is convergent by A1, A2, A17, Th33; :: thesis: verum
end;
A18: 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 x in dom ((lim (H1,X)) (#) (lim (H2,X))) ; :: thesis: ((lim (H1,X)) (#) (lim (H2,X))) . x = lim ((H1 (#) H2) # x)
then A19: x in (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:def 4;
then A20: x in dom (lim (H2,X)) by XBOOLE_0:def 4;
A21: x in dom (lim (H1,X)) by A19, XBOOLE_0:def 4;
then A22: x in X by A1, Def13;
then A23: ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th19;
thus ((lim (H1,X)) (#) (lim (H2,X))) . x = ((lim (H1,X)) . x) * ((lim (H2,X)) . x) by VALUED_1:5
.= (lim (H1 # x)) * ((lim (H2,X)) . x) by A1, A21, Def13
.= (lim (H1 # x)) * (lim (H2 # x)) by A2, A20, Def13
.= lim ((H1 # x) (#) (H2 # x)) by A23, SEQ_2:15
.= lim ((H1 (#) H2) # x) by A1, A2, A22, Th33 ; :: 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 VALUED_1:12;
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;
thus ((lim (H1,X)) - (lim (H2,X))) . x = ((lim (H1,X)) . x) - ((lim (H2,X)) . x) by A25, VALUED_1:13
.= (lim (H1 # x)) - ((lim (H2,X)) . x) by A1, A28, Def13
.= (lim (H1 # x)) - (lim (H2 # x)) by A2, A27, Def13
.= lim ((H1 # x) - (H2 # x)) by A30, SEQ_2:12
.= lim ((H1 - H2) # x) by A1, A2, A29, Th33 ; :: thesis: verum
end;
dom ((lim (H1,X)) + (lim (H2,X))) = (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_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)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) )
X common_on_dom H1 - H2 by A7, Th36;
hence A31: H1 - H2 is_point_conv_on X by A5, 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)) )
dom ((lim (H1,X)) - (lim (H2,X))) = (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:12
.= 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: ( H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) )
X common_on_dom H1 (#) H2 by A7, Th36;
hence A32: H1 (#) H2 is_point_conv_on X by A16, 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 VALUED_1:def 4
.= 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 A32, A18, Def13; :: thesis: verum