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