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: f . x = lim (H # x) by A1, A2, A3, Def14;
A6: H # x is convergent by A1, A4, 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 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
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 A8: ( 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: f = lim H,X

now

let x be Element of D; :: thesis: ( x in dom f implies f . x = lim (H # x) )
assume A9: x in dom f ; :: thesis: f . x = lim (H # x)

A10: 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 )
A11: p is Real by XREAL_0:def 1;
assume 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
then consider k being Element of NAT such that
A12: for n being Element of NAT st n >= k holds
abs (((H . n) . x) - (f . x)) < p by A8, A9, A11;
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 A12;
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 A10, SEQ_2:def 7; :: thesis: verum

end;

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