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

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