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 ;

A3: now :: thesis: for x being Element of D st x in dom (r (#) (lim (H,X))) holds
(r (#) (lim (H,X))) . x = lim ((r (#) H) # x)

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

end;

A8: now :: thesis: for x being Element of D st x in X holds
(r (#) H) # x is convergent

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, Th19;
then r (#) (H # x) is convergent by SEQ_2:7;
hence (r (#) H) # x is convergent by A2, A9, Th32; :: thesis: verum

end;

X common_on_dom r (#) H by A2, Th38;
hence A10: r (#) H is_point_conv_on X by A8, Th19; :: 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, Def13 ;
hence lim ((r (#) H),X) = r (#) (lim (H,X)) by A10, A3, Def13; :: thesis: verum