let D be non empty set ; :: thesis: for H being Functional_Sequence of D,REAL
for X being set
for f being PartFunc of D,REAL 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
let H be Functional_Sequence of D,REAL; :: thesis: for X being set
for f being PartFunc of D,REAL 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
let X be set ; :: thesis: for f being PartFunc of D,REAL 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) ) )
let f be PartFunc of D,REAL; :: 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ) )
hence A3: dom f = X by A1, Def14; :: thesis: for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p )
assume A4: x in X ; :: thesis: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
then A5: H # x is convergent by A1, Th21;
let p be Real; :: thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p )
assume A6: p > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
f . x = lim (H # x) by A1, A2, A3, A4, Def14;
then consider k being Element of NAT such that
A7: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p by A5, A6, SEQ_2:def 7;
take k ; :: thesis: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p
let n be Element of NAT ; :: thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p )
assume n >= k ; :: thesis: abs (((H . n) . x) - (f . x)) < p
then abs (((H # x) . n) - (f . x)) < p by A7;
hence abs (((H . n) . x) - (f . x)) < p by Def11; :: 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 Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p ; :: thesis: f = lim (H,X)

now

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)

A11: now

let p be real number ; :: thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p )
assume A12: p > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
p is Real by XREAL_0:def 1;
then consider k being Element of NAT such that
A13: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A8, A9, A10, A12;
take k = k; :: thesis: for n being Element of NAT st n >= k holds
abs (((H # x) . n) - (f . x)) < p
let n be Element of NAT ; :: thesis: ( n >= k implies abs (((H # x) . n) - (f . x)) < p )
assume n >= k ; :: thesis: abs (((H # x) . n) - (f . x)) < p
then abs (((H . n) . x) - (f . x)) < p by A13;
hence abs (((H # x) . n) - (f . x)) < p by Def11; :: thesis: verum

end;

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

end;

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