let X be non empty set ; :: thesis: for F, G being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds
( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )
let F, G be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X
for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds
( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )
let x be Element of X; :: thesis: for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds
( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )
let D be set ; :: thesis: ( ( for n being Nat holds G . n = (F . n) | D ) & x in D implies ( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) ) )
assume that
A1: for n being Nat holds G . n = (F . n) | D and
A2: x in D ; :: thesis: ( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )
thus A3: ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) :: thesis: ( ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )

proof

assume A4: F # x is convergent_to_+infty ; :: thesis: G # x is convergent_to_+infty
let g be Real; :: according to MESFUNC5:def 9 :: thesis: ( g <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or g <= (G # x) . b₂ ) )
assume 0 < g ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or g <= (G # x) . b₂ )
then consider n being Nat such that
A5: for m being Nat st n <= m holds
g <= (F # x) . m by A4;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or g <= (G # x) . b₁ )
let m be Nat; :: thesis: ( not n <= m or g <= (G # x) . m )
assume n <= m ; :: thesis: g <= (G # x) . m
then g <= (F # x) . m by A5;
then g <= (F . m) . x by MESFUNC5:def 13;
then g <= ((F . m) | D) . x by A2, FUNCT_1:49;
then g <= (G . m) . x by A1;
hence g <= (G # x) . m by MESFUNC5:def 13; :: thesis: verum

end;

thus A6: ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) :: thesis: ( ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )

proof

assume A7: F # x is convergent_to_-infty ; :: thesis: G # x is convergent_to_-infty
let g be Real; :: according to MESFUNC5:def 10 :: thesis: ( 0 <= g or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or (G # x) . b₂ <= g ) )
assume g < 0 ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or (G # x) . b₂ <= g )
then consider n being Nat such that
A8: for m being Nat st n <= m holds
(F # x) . m <= g by A7;
take n ; :: thesis: for b₁ being set holds
( not n <= b₁ or (G # x) . b₁ <= g )
let m be Nat; :: thesis: ( not n <= m or (G # x) . m <= g )
assume n <= m ; :: thesis: (G # x) . m <= g
then (F # x) . m <= g by A8;
then (F . m) . x <= g by MESFUNC5:def 13;
then ((F . m) | D) . x <= g by A2, FUNCT_1:49;
then (G . m) . x <= g by A1;
hence (G # x) . m <= g by MESFUNC5:def 13; :: thesis: verum

end;

thus A9: ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) :: thesis: ( F # x is convergent implies G # x is convergent )

proof

assume F # x is convergent_to_finite_number ; :: thesis: G # x is convergent_to_finite_number
then consider g being Real such that
A10: lim (F # x) = g and
A11: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((F # x) . m) - (lim (F # x))).| < p by Th7;
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p
then consider n being Nat such that
A12: for m being Nat st n <= m holds
|.(((F # x) . m) - (lim (F # x))).| < p by A11;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((G # x) . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((G # x) . m) - g).| < p )
(F # x) . m = (F . m) . x by MESFUNC5:def 13;
then (F # x) . m = ((F . m) | D) . x by A2, FUNCT_1:49;
then A13: (F # x) . m = (G . m) . x by A1;
assume n <= m ; :: thesis: |.(((G # x) . m) - g).| < p
then |.(((F # x) . m) - (lim (F # x))).| < p by A12;
hence |.(((G # x) . m) - g).| < p by A10, A13, MESFUNC5:def 13; :: thesis: verum

end;

hence G # x is convergent_to_finite_number ; :: thesis: verum

end;

assume A14: F # x is convergent ; :: thesis: G # x is convergent

per cases ( F # x is convergent_to_+infty or F # x is convergent_to_-infty or F # x is convergent_to_finite_number ) by A14;

suppose F # x is convergent_to_+infty ; :: thesis: G # x is convergent

hence G # x is convergent by A3; :: thesis: verum

end;

suppose F # x is convergent_to_-infty ; :: thesis: G # x is convergent

hence G # x is convergent by A6; :: thesis: verum

end;

suppose F # x is convergent_to_finite_number ; :: thesis: G # x is convergent

hence G # x is convergent by A9; :: thesis: verum

end;

end;