let seq be ExtREAL_sequence; :: thesis: Ser seq = Partial_Sums seq

for x being object st x in NAT holds

(Ser seq) . x = (Partial_Sums seq) . x

for x being object st x in NAT holds

(Ser seq) . x = (Partial_Sums seq) . x

proof

hence
Ser seq = Partial_Sums seq
by FUNCT_2:12; :: thesis: verum
defpred S_{1}[ Nat] means (Ser seq) . $1 = (Partial_Sums seq) . $1;

let x be object ; :: thesis: ( x in NAT implies (Ser seq) . x = (Partial_Sums seq) . x )

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then reconsider n = x as Element of NAT ;

(Ser seq) . 0 = seq . 0 by SUPINF_2:def 11

.= (Partial_Sums seq) . 0 by MESFUNC9:def 1 ;

then A2: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A2, A1);

then (Ser seq) . x = (Partial_Sums seq) . n ;

hence (Ser seq) . x = (Partial_Sums seq) . x ; :: thesis: verum

end;let x be object ; :: thesis: ( x in NAT implies (Ser seq) . x = (Partial_Sums seq) . x )

A1: for k being Nat st S

S

proof

assume
x in NAT
; :: thesis: (Ser seq) . x = (Partial_Sums seq) . x
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then (Ser seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SUPINF_2:def 11;

hence S_{1}[k + 1]
by MESFUNC9:def 1; :: thesis: verum

end;assume S

then (Ser seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SUPINF_2:def 11;

hence S

then reconsider n = x as Element of NAT ;

(Ser seq) . 0 = seq . 0 by SUPINF_2:def 11

.= (Partial_Sums seq) . 0 by MESFUNC9:def 1 ;

then A2: S

for k being Nat holds S

then (Ser seq) . x = (Partial_Sums seq) . n ;

hence (Ser seq) . x = (Partial_Sums seq) . x ; :: thesis: verum