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 )
assume A1: p = q ; :: thesis: Sum p = Sum q
consider P being Function of NAT ,ExtREAL such that
A2: ( Sum p = P . (len p) & P . 0 = 0. & ( for i being Element of NAT st i < len p holds
P . (i + 1) = (P . i) + (p . (i + 1)) ) ) by CONVFUN1:def 5;

now

per cases ( len q = 0 or len q <> 0 ) ;

case A3: len q = 0 ; :: thesis: Sum p = Sum q

Sum q = addreal "**" q by RVSUM_1:def 13;
hence Sum p = Sum q by A1, A2, A3, BINOP_2:2, FINSOP_1:def 1; :: thesis: verum

end;

case A4: len q <> 0 ; :: thesis: Sum p = Sum q

Sum q = addreal $$ q by RVSUM_1:def 13;
then consider Q being Function of NAT ,REAL such that
A5: ( Q . 1 = q . 1 & ( for n being Element of NAT st 0 <> n & n < len q holds
Q . (n + 1) = addreal . (Q . n),(q . (n + 1)) ) & Sum q = Q . (len q) ) by A4, FINSOP_1:def 1;
defpred S₁[ Nat] means ( 0 <> $1 & $1 <= len q implies P . $1 = Q . $1 );
A6: S₁[ 0 ] ;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
assume A9: ( 0 <> k + 1 & k + 1 <= len q ) ; :: thesis: P . (k + 1) = Q . (k + 1)
reconsider k = k as Element of NAT by ORDINAL1:def 13;

per cases ( k = 0 or k <> 0 ) ;

suppose A10: k = 0 ; :: thesis: P . (k + 1) = Q . (k + 1)

k < len q by A9, NAT_1:13;
then P . (k + 1) = (P . k) + (p . (k + 1)) by A1, A2
.= p . (k + 1) by A2, A10, XXREAL_3:4 ;
hence P . (k + 1) = Q . (k + 1) by A1, A5, A10; :: thesis: verum

end;

suppose A11: k <> 0 ; :: thesis: P . (k + 1) = Q . (k + 1)

A12: k < len q by A9, NAT_1:13;
then A13: P . (k + 1) = (P . k) + (p . (k + 1)) by A1, A2;
Q . (k + 1) = addreal . (Q . k),(q . (k + 1)) by A5, A11, A12
.= (Q . k) + (q . (k + 1)) by BINOP_2:def 9 ;
hence P . (k + 1) = Q . (k + 1) by A1, A8, A9, A11, A13, NAT_1:13, SUPINF_2:1; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
hence Sum p = Sum q by A1, A2, A4, A5; :: thesis: verum

end;

end;

end;

hence Sum p = Sum q ; :: thesis: verum