let D be non empty set ; :: thesis: for r being Real
for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
( r (#) H is_point_conv_on X & lim (r (#) H),X = r (#) (lim H,X) )
let r be Real; :: thesis: for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
( r (#) H is_point_conv_on X & lim (r (#) H),X = r (#) (lim H,X) )
let H be Functional_Sequence of D,REAL ; :: thesis: for X being set st H is_point_conv_on X holds
( r (#) H is_point_conv_on X & lim (r (#) H),X = r (#) (lim H,X) )
let X be set ; :: thesis: ( H is_point_conv_on X implies ( r (#) H is_point_conv_on X & lim (r (#) H),X = r (#) (lim H,X) ) )
assume A1: H is_point_conv_on X ; :: thesis: ( r (#) H is_point_conv_on X & lim (r (#) H),X = r (#) (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 r (#) H by Th40;

now

let x be Element of D; :: thesis: ( x in X implies (r (#) H) # x is convergent )
assume A4: x in X ; :: thesis: (r (#) H) # x is convergent
then H # x is convergent by A1, Th21;
then r (#) (H # x) is convergent by SEQ_2:21;
hence (r (#) H) # x is convergent by A2, A4, Th34; :: thesis: verum

end;

hence A5: r (#) H is_point_conv_on X by A3, Th21; :: thesis: lim (r (#) H),X = r (#) (lim H,X)
A6: dom (r (#) (lim H,X)) = dom (lim H,X) by VALUED_1:def 5
.= X by A1, Def14 ;

now

let x be Element of D; :: thesis: ( x in dom (r (#) (lim H,X)) implies (r (#) (lim H,X)) . x = lim ((r (#) H) # x) )
assume A7: x in dom (r (#) (lim H,X)) ; :: thesis: (r (#) (lim H,X)) . x = lim ((r (#) H) # x)
then A8: x in dom (lim H,X) by VALUED_1:def 5;
then A9: x in X by A1, Def14;
then A10: H # x is convergent by A1, Th21;
thus (r (#) (lim H,X)) . x = r * ((lim H,X) . x) by A7, VALUED_1:def 5
.= r * (lim (H # x)) by A1, A8, Def14
.= lim (r (#) (H # x)) by A10, SEQ_2:22
.= lim ((r (#) H) # x) by A2, A9, Th34 ; :: thesis: verum

end;

hence lim (r (#) H),X = r (#) (lim H,X) by A5, A6, Def14; :: thesis: verum