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₁[ 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₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of the carrier of V; :: thesis: for x being Element of V st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of V; :: 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 RLVECT_1:41
.= Sum (<*x*> ^ (Rev p)) by A2, RLVECT_1:41
.= Sum (Rev (p ^ <*x*>)) by FINSEQ_5:63 ; :: thesis: verum

end;

A3: S₁[ <*> the carrier of V] ;
thus for p being FinSequence of the carrier of V holds S₁[p] from FINSEQ_2:sch 2(A3, A1); :: thesis: verum