let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL

for n being Nat

for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let F be Functional_Sequence of X,REAL; :: thesis: for n being Nat

for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let n be Nat; :: thesis: for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let x be Element of X; :: thesis: for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let D be set ; :: thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D implies (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n )

assume ( F is with_the_same_dom & D c= dom (F . 0) & x in D ) ; :: thesis: (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

then (Partial_Sums ((R_EAL F) # x)) . n = ((Partial_Sums (R_EAL F)) # x) . n by Th9, MESFUNC9:32;

then (Partial_Sums (R_EAL (F # x))) . n = ((Partial_Sums (R_EAL F)) # x) . n by MESFUN7C:1;

then (R_EAL (Partial_Sums (F # x))) . n = ((Partial_Sums (R_EAL F)) # x) . n by Th5;

then (Partial_Sums (F # x)) . n = ((R_EAL (Partial_Sums F)) # x) . n by Th7;

hence (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by MESFUN7C:1; :: thesis: verum

for n being Nat

for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let F be Functional_Sequence of X,REAL; :: thesis: for n being Nat

for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let n be Nat; :: thesis: for x being Element of X

for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let x be Element of X; :: thesis: for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

let D be set ; :: thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D implies (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n )

assume ( F is with_the_same_dom & D c= dom (F . 0) & x in D ) ; :: thesis: (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

then (Partial_Sums ((R_EAL F) # x)) . n = ((Partial_Sums (R_EAL F)) # x) . n by Th9, MESFUNC9:32;

then (Partial_Sums (R_EAL (F # x))) . n = ((Partial_Sums (R_EAL F)) # x) . n by MESFUN7C:1;

then (R_EAL (Partial_Sums (F # x))) . n = ((Partial_Sums (R_EAL F)) # x) . n by Th5;

then (Partial_Sums (F # x)) . n = ((R_EAL (Partial_Sums F)) # x) . n by Th7;

hence (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by MESFUN7C:1; :: thesis: verum