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 S1[ 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 S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of the carrier of V; :: thesis: for x being Element of V st S1[p] holds
S1[p ^ <*x*>]
let x be Element of V; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: Sum p = Sum (Rev p) ; :: thesis: S1[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: S1[ <*> the carrier of V] ;
thus for p being FinSequence of the carrier of V holds S1[p] from FINSEQ_2:sch 2(A3, A1); :: thesis: verum