let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
let F be Functional_Sequence of X,REAL; :: thesis: for x being Element of X
for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
let x be Element of X; :: thesis: for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent
let D be set ; :: thesis: ( x in D & F # x is convergent implies (F || D) # x is convergent )
set G = F || D;
assume A1: x in D ; :: thesis: ( not F # x is convergent or (F || D) # x is convergent )
A2: (R_EAL (F || D)) # x = (F || D) # x by MESFUN7C:1;
assume F # x is convergent ; :: thesis: (F || D) # x is convergent
then R_EAL (F # x) is convergent_to_finite_number by RINFSUP2:14;
then A3: (R_EAL F) # x is convergent_to_finite_number by MESFUN7C:1;
for n being Nat holds (R_EAL (F || D)) . n = ((R_EAL F) . n) | D by Def1;
then (R_EAL (F || D)) # x is convergent_to_finite_number by A1, A3, MESFUNC9:12;
hence (F || D) # x is convergent by A2, RINFSUP2:15; :: thesis: verum