let X be non empty set ; :: thesis: for F being summable FinSequence of Funcs (X,ExtREAL) holds
( dom F = dom (Partial_Sums F) & ( for n being Nat st n in dom F holds
(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) ) )
let F be summable FinSequence of Funcs (X,ExtREAL); :: thesis: ( dom F = dom (Partial_Sums F) & ( for n being Nat st n in dom F holds
(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) ) )
len F = len (Partial_Sums F) by MEASUR11:def 11;
hence A1: dom F = dom (Partial_Sums F) by FINSEQ_3:29; :: thesis: ( ( for n being Nat st n in dom F holds
(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) ) )
hence for n being Nat st n in dom F holds
(Partial_Sums F) /. n = (Partial_Sums F) . n by PARTFUN1:def 6; :: thesis: for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x)
thus for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) :: thesis: verum

proof

let n be Nat; :: thesis: for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x)
let x be Element of X; :: thesis: ( 1 <= n & n < len F implies ((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) )
assume A3: ( 1 <= n & n < len F ) ; :: thesis: ((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x)
then ( 1 <= n + 1 & n + 1 <= len F ) by NAT_1:13;
then A4: (Partial_Sums F) /. (n + 1) = (Partial_Sums F) . (n + 1) by A1, PARTFUN1:def 6, FINSEQ_3:25
.= ((Partial_Sums F) /. n) + (F /. (n + 1)) by A3, MEASUR11:def 11 ;
dom ((Partial_Sums F) /. (n + 1)) = X by FUNCT_2:def 1;
hence ((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. n) . x) + ((F /. (n + 1)) . x) by A4, MESFUNC1:def 3; :: thesis: verum

end;