let D be non empty set ; :: thesis: for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
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 Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
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 Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
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, the carrier of Y; :: 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)) )

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 VFUNCT_1:def 4;
then A6: x in X by A1, Def13;
X1: (lim (H,X)) /. x = (lim (H,X)) . x by PARTFUN1:def 6, A5;
X2: (r (#) (lim (H,X))) . x = (r (#) (lim (H,X))) /. x by PARTFUN1:def 6, A4;
thus (r (#) (lim (H,X))) . x = r * ((lim (H,X)) /. x) by X2, A4, VFUNCT_1:def 4
.= r * (lim (H # x)) by A1, A5, X1, Def13
.= lim (r * (H # x)) by A6, A1, Th19, NORMSP_1:28
.= lim ((r (#) H) # x) by A1, 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 r * (H # x) is convergent by A1, Th19, NORMSP_1:22;
hence (r (#) H) # x is convergent by A1, A9, Th32; :: thesis: verum

end;

A10: r (#) H is_point_conv_on X by A1, Th38, A8, Th19;
dom (r (#) (lim (H,X))) = dom (lim (H,X)) by VFUNCT_1:def 4
.= X by A1, Def13 ;
hence ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) by A10, A3, Def13; :: thesis: verum