let V be non empty Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)

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

A1: for p being FinSequence of the carrier of V

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

S_{1}[p ^ <*x*>]
_{1}[ <*> the carrier of V]
;

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

defpred S

A1: for p being FinSequence of the carrier of V

for x being Element of V st S

S

proof

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

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

let x be Element of V; :: 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 RLVECT_1:41

.= Sum (<*x*> ^ (Rev p)) by A2, RLVECT_1:41

.= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; :: thesis: verum

end;S

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

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

thus Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RLVECT_1:41

.= Sum (<*x*> ^ (Rev p)) by A2, RLVECT_1:41

.= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; :: thesis: verum

thus for p being FinSequence of the carrier of V holds S