let D be non empty set ; 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; 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; 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 ; ( 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
; ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) )
then A2:
X common_on_dom H
;
A3:
now 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;
( 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)))
;
(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
;
verum end;
X common_on_dom r (#) H
by A2, Th38;
hence A10:
r (#) H is_point_conv_on X
by A8, Th19; 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; verum