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

for f being PartFunc of X,REAL

for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let F be Functional_Sequence of X,REAL; :: thesis: for f being PartFunc of X,REAL

for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let f be PartFunc of X,REAL; :: thesis: for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let x be Element of X; :: thesis: ( F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) implies f . x = lim ((Partial_Sums F) # x) )

assume that

A1: ( F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f ) and

A2: f . x = Sum (F # x) ; :: thesis: f . x = lim ((Partial_Sums F) # x)

A3: ( dom (Partial_Sums (F # x)) = NAT & dom ((Partial_Sums F) # x) = NAT ) by FUNCT_2:def 1;

for n being object st n in NAT holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by A1, Th12;

hence f . x = lim ((Partial_Sums F) # x) by A2, A3, FUNCT_1:2; :: thesis: verum

for f being PartFunc of X,REAL

for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let F be Functional_Sequence of X,REAL; :: thesis: for f being PartFunc of X,REAL

for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let f be PartFunc of X,REAL; :: thesis: for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

f . x = lim ((Partial_Sums F) # x)

let x be Element of X; :: thesis: ( F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) implies f . x = lim ((Partial_Sums F) # x) )

assume that

A1: ( F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f ) and

A2: f . x = Sum (F # x) ; :: thesis: f . x = lim ((Partial_Sums F) # x)

A3: ( dom (Partial_Sums (F # x)) = NAT & dom ((Partial_Sums F) # x) = NAT ) by FUNCT_2:def 1;

for n being object st n in NAT holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by A1, Th12;

hence f . x = lim ((Partial_Sums F) # x) by A2, A3, FUNCT_1:2; :: thesis: verum