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 Nat st
for n being Nat st n >= k holds
|.(((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 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,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 Nat st
for n being Nat st n >= k holds
|.(((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 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;
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 A5, A6, SEQ_2:def 7;
reconsider k = k as Nat ;
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)

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 A12: p > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
|.(((H # x) . n) - (f . x)).| < p
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, A12;
reconsider k = k as Nat ;
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 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, Def13; :: thesis: verum