defpred S_{1}[ FinSequence of REAL ] means Sum $1 = Sum (Rev $1);

A1: for p being FinSequence of REAL

for x being Element of REAL st S_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[ <*> REAL]
;

thus for p being FinSequence of REAL holds S_{1}[p]
from FINSEQ_2:sch 2(A3, A1); :: thesis: verum

A1: for p being FinSequence of REAL

for x being Element of REAL st S

S

proof

A3:
S
let p be FinSequence of REAL ; :: thesis: for x being Element of REAL st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be Element of REAL ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

assume A2: Sum p = Sum (Rev p) ; :: thesis: S_{1}[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;S

let x be Element of REAL ; :: thesis: ( S

assume A2: Sum p = Sum (Rev p) ; :: thesis: S

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

thus for p being FinSequence of REAL holds S