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 = abs (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 = abs (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 = abs (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 = abs (lim H,X) & - H is_point_conv_on X & lim (- H),X = - (lim H,X) )

A2: now

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, Th21;
then abs (H # x) is convergent by SEQ_4:26;
hence (abs H) # x is convergent by Th33; :: thesis: verum

end;

A3: now

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, Def14;
then A5: H # x is convergent by A1, Th21;
thus (- (lim H,X)) . x = - ((lim H,X) . x) by VALUED_1:8
.= - (lim (H # x)) by A1, A4, Def14
.= lim (- (H # x)) by A5, SEQ_2:24
.= lim ((- H) # x) by Th33 ; :: thesis: verum

end;

A6: X common_on_dom H by A1, Th21;
then X common_on_dom abs H by Th39;
hence A7: abs H is_point_conv_on X by A2, Th21; :: thesis: ( lim (abs H),X = abs (lim H,X) & - H is_point_conv_on X & lim (- H),X = - (lim H,X) )

A8: now

let x be Element of D; :: thesis: ( x in dom (abs (lim H,X)) implies (abs (lim H,X)) . x = lim ((abs H) # x) )
assume x in dom (abs (lim H,X)) ; :: thesis: (abs (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, Def14;
then A10: H # x is convergent by A1, Th21;
thus (abs (lim H,X)) . x = abs ((lim H,X) . x) by VALUED_1:18
.= abs (lim (H # x)) by A1, A9, Def14
.= lim (abs (H # x)) by A10, SEQ_4:27
.= lim ((abs H) # x) by Th33 ; :: thesis: verum

end;

A11: now

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, Th21;
then - (H # x) is convergent by SEQ_2:23;
hence (- H) # x is convergent by Th33; :: thesis: verum

end;

dom (abs (lim H,X)) = dom (lim H,X) by VALUED_1:def 11
.= X by A1, Def14 ;
hence lim (abs H),X = abs (lim H,X) by A7, A8, Def14; :: thesis: ( - H is_point_conv_on X & lim (- H),X = - (lim H,X) )
X common_on_dom - H by A6, Th39;
hence A12: - H is_point_conv_on X by A11, Th21; :: thesis: lim (- H),X = - (lim H,X)
dom (- (lim H,X)) = dom (lim H,X) by VALUED_1:8
.= X by A1, Def14 ;
hence lim (- H),X = - (lim H,X) by A12, A3, Def14; :: thesis: verum