let p be REAL -valued FinSequence; :: thesis: Sum p = Sum (Rev p)
A0: p is FinSequence of REAL by RVSUM_1:145;
defpred S₁[ FinSequence of REAL ] means Sum $1 = Sum (Rev $1);
A1: for p being FinSequence of REAL
for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of REAL ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A2: Sum p = Sum (Rev p) ; :: thesis: S₁[p ^ <*x*>]
thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RVSUM_1:75
.= Sum (<*x*> ^ (Rev p)) by A2, RVSUM_1:75
.= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; :: thesis: verum

end;

A3: S₁[ <*> REAL] ;
for p being FinSequence of REAL holds S₁[p] from FINSEQ_2:sch 2(A3, A1);
hence Sum p = Sum (Rev p) by A0; :: thesis: verum