let p be FinSequence of ExtREAL ; :: thesis: for q being FinSequence of REAL st p = q holds
Sum p = Sum q
let q be FinSequence of REAL ; :: thesis: ( p = q implies Sum p = Sum q )
consider P being Function of NAT,ExtREAL such that
A1: Sum p = P . (len p) and
A2: P . 0 = 0. and
A3: for i being Element of NAT st i < len p holds
P . (i + 1) = (P . i) + (p . (i + 1)) by EXTREAL1:def 2;
assume A4: p = q ; :: thesis: Sum p = Sum q
now
per cases ( len q = 0 or len q <> 0 ) ;
case A6: len q <> 0 ; :: thesis: Sum p = Sum q
Sum q = addreal $$ q by RVSUM_1:def 12;
then consider Q being Function of NAT,REAL such that
A7: Q . 1 = q . 1 and
A8: for n being Element of NAT st 0 <> n & n < len q holds
Q . (n + 1) = addreal . ((Q . n),(q . (n + 1))) and
A9: Sum q = Q . (len q) by A6, FINSOP_1:def 1;
defpred S1[ Nat] means ( 0 <> $1 & $1 <= len q implies P . $1 = Q . $1 );
A10: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
assume that
0 <> k + 1 and
A12: k + 1 <= len q ; :: thesis: P . (k + 1) = Q . (k + 1)
reconsider k = k as Element of NAT by ORDINAL1:def 12;
per cases ( k = 0 or k <> 0 ) ;
suppose A13: k = 0 ; :: thesis: P . (k + 1) = Q . (k + 1)
k < len q by A12, NAT_1:13;
then P . (k + 1) = (P . k) + (p . (k + 1)) by A4, A3
.= p . (k + 1) by A2, A13, XXREAL_3:4 ;
hence P . (k + 1) = Q . (k + 1) by A4, A7, A13; :: thesis: verum
end;
suppose A14: k <> 0 ; :: thesis: P . (k + 1) = Q . (k + 1)
A15: k < len q by A12, NAT_1:13;
then A16: Q . (k + 1) = addreal . ((Q . k),(q . (k + 1))) by A8, A14
.= (Q . k) + (q . (k + 1)) by BINOP_2:def 9 ;
P . (k + 1) = (P . k) + (p . (k + 1)) by A4, A3, A15;
hence P . (k + 1) = Q . (k + 1) by A4, A11, A12, A14, A16, NAT_1:13, SUPINF_2:1; :: thesis: verum
end;
end;
end;
A17: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A17, A10);
hence Sum p = Sum q by A4, A1, A6, A9; :: thesis: verum
end;
end;
end;
hence Sum p = Sum q ; :: thesis: verum