let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
( abs H is_point_conv_on X & lim ((abs H),X) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
let H be Functional_Sequence of D,REAL; :: thesis: for X being set st H is_point_conv_on X holds
( abs H is_point_conv_on X & lim ((abs H),X) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
let X be set ; :: thesis: ( H is_point_conv_on X implies ( abs H is_point_conv_on X & lim ((abs H),X) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) )
assume A1: H is_point_conv_on X ; :: thesis: ( abs H is_point_conv_on X & lim ((abs H),X) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
A2: now :: thesis: for x being Element of D st x in X holds
(abs H) # x is convergent
let x be Element of D; :: thesis: ( x in X implies (abs H) # x is convergent )
assume x in X ; :: thesis: (abs H) # x is convergent
then H # x is convergent by A1, Th19;
then abs (H # x) is convergent by SEQ_4:13;
hence (abs H) # x is convergent by Th31; :: thesis: verum
end;
A3: now :: thesis: for x being Element of D st x in dom (- (lim (H,X))) holds
(- (lim (H,X))) . x = lim ((- H) # x)
let x be Element of D; :: thesis: ( x in dom (- (lim (H,X))) implies (- (lim (H,X))) . x = lim ((- H) # x) )
assume x in dom (- (lim (H,X))) ; :: thesis: (- (lim (H,X))) . x = lim ((- H) # x)
then A4: x in dom (lim (H,X)) by VALUED_1:8;
then x in X by A1, Def13;
then A5: H # x is convergent by A1, Th19;
thus (- (lim (H,X))) . x = - ((lim (H,X)) . x) by VALUED_1:8
.= - (lim (H # x)) by A1, A4, Def13
.= lim (- (H # x)) by A5, SEQ_2:10
.= lim ((- H) # x) by Th31 ; :: thesis: verum
end;
A6: X common_on_dom H by A1;
then X common_on_dom abs H by Th37;
hence A7: abs H is_point_conv_on X by A2, Th19; :: thesis: ( lim ((abs H),X) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
A8: now :: thesis: for x being Element of D st x in dom |.(lim (H,X)).| holds
|.(lim (H,X)).| . x = lim ((abs H) # x)
let x be Element of D; :: thesis: ( x in dom |.(lim (H,X)).| implies |.(lim (H,X)).| . x = lim ((abs H) # x) )
assume x in dom |.(lim (H,X)).| ; :: thesis: |.(lim (H,X)).| . x = lim ((abs H) # x)
then A9: x in dom (lim (H,X)) by VALUED_1:def 11;
then x in X by A1, Def13;
then A10: H # x is convergent by A1, Th19;
thus |.(lim (H,X)).| . x = |.((lim (H,X)) . x).| by VALUED_1:18
.= |.(lim (H # x)).| by A1, A9, Def13
.= lim |.(H # x).| by A10, SEQ_4:14
.= lim ((abs H) # x) by Th31 ; :: thesis: verum
end;
A11: now :: thesis: for x being Element of D st x in X holds
(- H) # x is convergent
let x be Element of D; :: thesis: ( x in X implies (- H) # x is convergent )
assume x in X ; :: thesis: (- H) # x is convergent
then H # x is convergent by A1, Th19;
then - (H # x) is convergent by SEQ_2:9;
hence (- H) # x is convergent by Th31; :: thesis: verum
end;
dom |.(lim (H,X)).| = dom (lim (H,X)) by VALUED_1:def 11
.= X by A1, Def13 ;
hence lim ((abs H),X) = |.(lim (H,X)).| by A7, A8, Def13; :: thesis: ( - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )
X common_on_dom - H by A6, Th37;
hence A12: - H is_point_conv_on X by A11, Th19; :: thesis: lim ((- H),X) = - (lim (H,X))
dom (- (lim (H,X))) = dom (lim (H,X)) by VALUED_1:8
.= X by A1, Def13 ;
hence lim ((- H),X) = - (lim (H,X)) by A12, A3, Def13; :: thesis: verum