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 by Th21;

A3: 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 A4: x in dom (r (#) (lim (H,X))) ; :: thesis: (r (#) (lim (H,X))) . x = lim ((r (#) H) # x)
then A5: x in dom (lim (H,X)) by VALUED_1:def 5;
then A6: x in X by A1, Def14;
then A7: H # x is convergent by A1, Th21;
thus (r (#) (lim (H,X))) . x = r * ((lim (H,X)) . x) by A4, VALUED_1:def 5
.= r * (lim (H # x)) by A1, A5, Def14
.= lim (r (#) (H # x)) by A7, SEQ_2:8
.= lim ((r (#) H) # x) by A2, A6, Th34 ; :: thesis: verum

end;

A8: now

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

end;

X common_on_dom r (#) H by A2, Th40;
hence A10: r (#) H is_point_conv_on X by A8, Th21; :: thesis: lim ((r (#) H),X) = r (#) (lim (H,X))
dom (r (#) (lim (H,X))) = dom (lim (H,X)) by VALUED_1:def 5
.= X by A1, Def14 ;
hence lim ((r (#) H),X) = r (#) (lim (H,X)) by A10, A3, Def14; :: thesis: verum