let D be non empty set ; :: thesis: for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set
for f being PartFunc of D, the carrier of Y st H is_point_conv_on X holds
( f = lim (H,X) iff ( dom f = X & ( 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 ) ) )
let Y be RealNormSpace; :: thesis: for H being Functional_Sequence of D, the carrier of Y
for X being set
for f being PartFunc of D, the carrier of Y st H is_point_conv_on X holds
( f = lim (H,X) iff ( dom f = X & ( 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 ) ) )
let H be Functional_Sequence of D, the carrier of Y; :: thesis: for X being set
for f being PartFunc of D, the carrier of Y st H is_point_conv_on X holds
( f = lim (H,X) iff ( dom f = X & ( 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 ) ) )
let X be set ; :: thesis: for f being PartFunc of D, the carrier of Y st H is_point_conv_on X holds
( f = lim (H,X) iff ( dom f = X & ( 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 ) ) )
let f be PartFunc of D, the carrier of Y; :: thesis: ( H is_point_conv_on X implies ( f = lim (H,X) iff ( dom f = X & ( 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 ) ) ) )
assume A1: H is_point_conv_on X ; :: thesis: ( f = lim (H,X) iff ( dom f = X & ( 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 ) ) )
thus ( f = lim (H,X) implies ( dom f = X & ( 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 ) ) ) :: thesis: ( dom f = X & ( 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 ) implies f = lim (H,X) )

proof

assume A2: f = lim (H,X) ; :: thesis: ( dom f = X & ( 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 ) )
hence A3: dom f = X by A1, Def13; :: thesis: 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
let x be Element of D; :: thesis: ( x in X 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) - (f /. x)).|| < p )
assume A4: x in X ; :: thesis: 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
then A5: H # x is convergent by A1, Th19;
X6: f /. x = f . x by PARTFUN1:def 6, A4, A3;
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p )
assume A6: p > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
f . x = lim (H # x) by A1, A2, A3, A4, Def13;
then consider k being Nat such that
A7: for n being Nat st n >= k holds
||.(((H # x) . n) - (f /. x)).|| < p by X6, A5, A6, NORMSP_1:def 7;
take k ; :: thesis: for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
let n be Nat; :: thesis: ( n >= k implies ||.(((H . n) /. x) - (f /. x)).|| < p )
assume n >= k ; :: thesis: ||.(((H . n) /. x) - (f /. x)).|| < p
then ||.(((H # x) . n) - (f /. x)).|| < p by A7;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by Def10; :: thesis: verum

end;

assume that
A8: dom f = X and
A9: 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 ; :: thesis: f = lim (H,X)

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

let x be Element of D; :: thesis: ( x in dom f implies f . x = lim (H # x) )
assume A10: x in dom f ; :: thesis: f . x = lim (H # x)
X10: f /. x = f . x by A10, PARTFUN1:def 6;

A11: now :: thesis: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H # x) . n) - (f /. x)).|| < p

let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.(((H # x) . n) - (f /. x)).|| < p )
assume p > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.(((H # x) . n) - (f /. x)).|| < p
then consider k being Nat such that
A13: for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p by A8, A9, A10;
take k = k; :: thesis: for n being Nat st n >= k holds
||.(((H # x) . n) - (f /. x)).|| < p
let n be Nat; :: thesis: ( n >= k implies ||.(((H # x) . n) - (f /. x)).|| < p )
assume n >= k ; :: thesis: ||.(((H # x) . n) - (f /. x)).|| < p
then ||.(((H . n) /. x) - (f /. x)).|| < p by A13;
hence ||.(((H # x) . n) - (f /. x)).|| < p by Def10; :: thesis: verum

end;

then H # x is convergent by NORMSP_1:def 6;
hence f . x = lim (H # x) by X10, A11, NORMSP_1:def 7; :: thesis: verum

end;

hence f = lim (H,X) by A1, A8, Def13; :: thesis: verum