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 A0: 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 number ;

Q00: now

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

hereby :: thesis: verum

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

end;

end;

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

end;

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

now

let e be real number ; :: 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
Q02: for n being Nat
for x being set st n >= N & x in dom (F1 . 0 ) holds
|.(((F1 . n) . x) - (f . x)).| < e by A0, DefUC;
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 Q02, A2;
then P03: |.(- (((F1 . n) . x) - (f . x))).| < e by EXTREAL2:66;
(F1 . n) . x = (F1 # x) . n by MESFUNC5:def 13;
then - (((F1 # x) . n) - (f . x)) < R_EAL e by P03, EXTREAL2:58;
then (f . x) - ((F1 # x) . n) < R_EAL e by XXREAL_3:27;
then (F1 # x) . n = +infty by P2, XXREAL_3:65;
hence e <= (F1 # x) . n by XXREAL_0:3; :: thesis: verum

end;

end;

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

end;

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

now

let e be real number ; :: 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:26;
then consider N being Nat such that
Q03: for n being Nat
for x being set st n >= N & x in dom (F1 . 0 ) holds
|.(((F1 . n) . x) - (f . x)).| < - e by A0, DefUC;
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 P03: |.(((F1 . n) . x) - (f . x)).| < - e by Q03, A2;
(F1 . n) . x = (F1 # x) . n by MESFUNC5:def 13;
then ((F1 # x) . n) - (f . x) < R_EAL (- e) by P03, EXTREAL2:58;
then (F1 # x) . n = -infty by P3, XXREAL_3:65;
hence e >= (F1 # x) . n by XXREAL_0:5; :: thesis: verum

end;

end;

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

end;

end;