let X be non empty set ; :: thesis: for F1 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds
for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
let F1 be Functional_Sequence of X,ExtREAL; :: thesis: for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds
for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
let f be PartFunc of X,ExtREAL; :: thesis: ( F1 is_uniformly_convergent_to f implies for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x ) )
assume A1: F1 is_uniformly_convergent_to f ; :: thesis: for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
let x be Element of X; :: thesis: ( x in dom (F1 . 0) implies ( F1 # x is convergent & lim (F1 # x) = f . x ) )
assume A2: x in dom (F1 . 0) ; :: thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )

per cases ( f . x in REAL or f . x = +infty or f . x = -infty ) by XXREAL_0:14;

suppose f . x in REAL ; :: thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )

then reconsider g = f . x as Real ;

A3: now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for m being Nat st N <= m holds
|.(((F1 # x) . m) - g).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for m being Nat st N <= m holds
|.(((F1 # x) . m) - g).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
|.(((F1 # x) . m) - g).| < e
then consider N being Nat such that
A4: for n being Nat
for x being set st n >= N & x in dom (F1 . 0) holds
|.(((F1 . n) . x) - (f . x)).| < e by A1;
take N = N; :: thesis: for m being Nat st N <= m holds
|.(((F1 # x) . m) - g).| < e

hereby :: thesis: verum

let m be Nat; :: thesis: ( N <= m implies |.(((F1 # x) . m) - g).| < e )
assume N <= m ; :: thesis: |.(((F1 # x) . m) - g).| < e
then |.(((F1 . m) . x) - (f . x)).| < e by A2, A4;
hence |.(((F1 # x) . m) - g).| < e by MESFUNC5:def 13; :: thesis: verum

end;

end;

then A5: F1 # x is convergent_to_finite_number ;
then F1 # x is convergent ;
hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A3, A5, MESFUNC5:def 12; :: thesis: verum

end;

suppose A6: f . x = +infty ; :: thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )

now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
e <= (F1 # x) . n

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
e <= (F1 # x) . n )
assume 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
e <= (F1 # x) . n
then consider N being Nat such that
A7: for n being Nat
for x being set st n >= N & x in dom (F1 . 0) holds
|.(((F1 . n) . x) - (f . x)).| < e by A1;
take N = N; :: thesis: for n being Nat st n >= N holds
e <= (F1 # x) . n

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies e <= (F1 # x) . n )
assume n >= N ; :: thesis: e <= (F1 # x) . n
then |.(((F1 . n) . x) - (f . x)).| < e by A2, A7;
then A8: |.(- (((F1 . n) . x) - (f . x))).| < e by EXTREAL1:29;
(F1 . n) . x = (F1 # x) . n by MESFUNC5:def 13;
then - (((F1 # x) . n) - (f . x)) < e by A8, EXTREAL1:21;
then (f . x) - ((F1 # x) . n) < e by XXREAL_3:26;
then (F1 # x) . n = +infty by A6, XXREAL_3:54;
hence e <= (F1 # x) . n by XXREAL_0:3; :: thesis: verum

end;

end;

then A9: F1 # x is convergent_to_+infty ;
then F1 # x is convergent ;
hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A6, A9, MESFUNC5:def 12; :: thesis: verum

end;

suppose A10: f . x = -infty ; :: thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )

now :: thesis: for e being Real st e < 0 holds
ex N being Nat st
for n being Nat st n >= N holds
e >= (F1 # x) . n

let e be Real; :: thesis: ( e < 0 implies ex N being Nat st
for n being Nat st n >= N holds
e >= (F1 # x) . n )
assume e < 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
e >= (F1 # x) . n
then - 0 < - e by XREAL_1:24;
then consider N being Nat such that
A11: for n being Nat
for x being set st n >= N & x in dom (F1 . 0) holds
|.(((F1 . n) . x) - (f . x)).| < - e by A1;
take N = N; :: thesis: for n being Nat st n >= N holds
e >= (F1 # x) . n

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies e >= (F1 # x) . n )
assume n >= N ; :: thesis: e >= (F1 # x) . n
then A12: |.(((F1 . n) . x) - (f . x)).| < - e by A2, A11;
(F1 . n) . x = (F1 # x) . n by MESFUNC5:def 13;
then ((F1 # x) . n) - (f . x) < - e by A12, EXTREAL1:21;
then (F1 # x) . n = -infty by A10, XXREAL_3:54;
hence e >= (F1 # x) . n by XXREAL_0:5; :: thesis: verum

end;

end;

then A13: F1 # x is convergent_to_-infty ;
then F1 # x is convergent ;
hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A10, A13, MESFUNC5:def 12; :: thesis: verum

end;

end;