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) )
then A2: ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) ) by Th21;
then A3: X common_on_dom abs H by Th39;

now

let x be Element of D; :: thesis: ( x in X implies (abs H) # x is convergent )
assume A4: 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 A2, A4, Th33; :: thesis: verum

end;

hence A5: abs H is_point_conv_on X by A3, Th21; :: thesis: ( lim (abs H),X = abs (lim H,X) & - H is_point_conv_on X & lim (- H),X = - (lim H,X) )
A6: dom (abs (lim H,X)) = dom (lim H,X) by VALUED_1:def 11
.= X by A1, Def14 ;

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 A7: x in dom (lim H,X) by VALUED_1:def 11;
then A8: x in X by A1, Def14;
then A9: 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, A7, Def14
.= lim (abs (H # x)) by A9, SEQ_4:27
.= lim ((abs H) # x) by A1, A8, Th36 ; :: thesis: verum

end;

hence lim (abs H),X = abs (lim H,X) by A5, A6, Def14; :: thesis: ( - H is_point_conv_on X & lim (- H),X = - (lim H,X) )
A10: X common_on_dom - H by A2, Th39;

now

let x be Element of D; :: thesis: ( x in X implies (- H) # x is convergent )
assume A11: 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 A2, A11, Th33; :: thesis: verum

end;

hence A12: - H is_point_conv_on X by A10, Th21; :: thesis: lim (- H),X = - (lim H,X)
A13: dom (- (lim H,X)) = dom (lim H,X) by VALUED_1:8
.= X by A1, Def14 ;

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 A14: x in dom (lim H,X) by VALUED_1:8;
then A15: x in X by A1, Def14;
then A16: 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, A14, Def14
.= lim (- (H # x)) by A16, SEQ_2:24
.= lim ((- H) # x) by A1, A15, Th36 ; :: thesis: verum

end;

hence lim (- H),X = - (lim H,X) by A12, A13, Def14; :: thesis: verum