let D be non empty set ; for Z being set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let Z be set ; for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let Y be RealNormSpace; for H being Functional_Sequence of D, the carrier of Y
for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let H be Functional_Sequence of D, the carrier of Y; for X being set st Z c= X & Z <> {} & H is_point_conv_on X holds
( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
let X be set ; ( Z c= X & Z <> {} & H is_point_conv_on X implies ( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) ) )
assume that
A1:
Z c= X
and
A2:
Z <> {}
and
A3:
H is_point_conv_on X
; ( H is_point_conv_on Z & (lim (H,X)) | Z = lim (H,Z) )
consider f being PartFunc of D, the carrier of Y such that
A4:
X = dom f
and
A5:
for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
by A3;
now ex g being Element of K16(K17(D, the carrier of Y)) st
( Z = dom g & ( for x being Element of D st x in Z holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < p ) )take g =
f | Z;
( Z = dom g & ( for x being Element of D st x in Z holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < p ) )thus A7:
Z = dom g
by A1, A4, RELAT_1:62;
for x being Element of D st x in Z holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < plet x be
Element of
D;
( x in Z implies for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < p )assume A8:
x in Z
;
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < pthen X8:
f /. x = f . x
by A1, A4, PARTFUN1:def 6;
g /. x = g . x
by A7, A8, PARTFUN1:def 6;
then X10:
g /. x = f /. x
by A7, A8, FUNCT_1:47, X8;
let p be
Real;
( p > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < p )assume
p > 0
;
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < pthen consider k being
Nat such that A9:
for
n being
Nat st
n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
by A1, A5, A8;
take k =
k;
for n being Nat st n >= k holds
||.(((H . n) /. x) - (g /. x)).|| < plet n be
Nat;
( n >= k implies ||.(((H . n) /. x) - (g /. x)).|| < p )assume
n >= k
;
||.(((H . n) /. x) - (g /. x)).|| < phence
||.(((H . n) /. x) - (g /. x)).|| < p
by A9, X10;
verum end;
hence A10:
H is_point_conv_on Z
by A1, A2, A3, Th22; (lim (H,X)) | Z = lim (H,Z)
A11:
now for x being Element of D st x in dom ((lim (H,X)) | Z) holds
((lim (H,X)) | Z) . x = (lim (H,Z)) . xlet x be
Element of
D;
( x in dom ((lim (H,X)) | Z) implies ((lim (H,X)) | Z) . x = (lim (H,Z)) . x )assume A12:
x in dom ((lim (H,X)) | Z)
;
((lim (H,X)) | Z) . x = (lim (H,Z)) . xthen A13:
x in (dom (lim (H,X))) /\ Z
by RELAT_1:61;
then A14:
x in dom (lim (H,X))
by XBOOLE_0:def 4;
x in Z
by A13, XBOOLE_0:def 4;
then A15:
x in dom (lim (H,Z))
by A10, Def13;
thus ((lim (H,X)) | Z) . x =
(lim (H,X)) . x
by A12, FUNCT_1:47
.=
lim (H # x)
by A3, A14, Def13
.=
(lim (H,Z)) . x
by A10, A15, Def13
;
verum end;
dom (lim (H,X)) = X
by A3, Def13;
then
(dom (lim (H,X))) /\ Z = Z
by A1, XBOOLE_1:28;
then
dom ((lim (H,X)) | Z) = Z
by RELAT_1:61;
then
dom ((lim (H,X)) | Z) = dom (lim (H,Z))
by A10, Def13;
hence
(lim (H,X)) | Z = lim (H,Z)
by A11, PARTFUN1:5; verum