let k be positive Nat; :: thesis: Sum (powersFS ((- k),3,((2 * k) - 1))) = 0
defpred S₁[ non zero Nat] means Sum (powersFS ((- $1),3,((2 * $1) - 1))) = 0 ;
A1: S₁[1]

proof

set f = powersFS ((- 1),3,((2 * 1) - 1));
( len (powersFS ((- 1),3,((2 * 1) - 1))) = 1 & (powersFS ((- 1),3,((2 * 1) - 1))) . 1 = ((- 1) + 1) to_power 3 ) by Def7;
then powersFS ((- 1),3,((2 * 1) - 1)) = <*0*> by FINSEQ_1:40;
hence Sum (powersFS ((- 1),3,((2 * 1) - 1))) = 0 ; :: thesis: verum

end;

A2: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set f = powersFS ((- (n + 1)),3,((2 * (n + 1)) - 1));
set g = powersFS ((- n),3,((2 * n) - 1));
set a = (- n) to_power 3;
set b = n to_power 3;
A4: Sum (<*((- n) to_power 3)*> ^ (powersFS ((- n),3,((2 * n) - 1)))) = ((- n) to_power 3) + (Sum (powersFS ((- n),3,((2 * n) - 1)))) by RVSUM_1:76;
A5: ( (- n) to_power 3 = ((- n) * (- n)) * (- n) & n to_power 3 = (n * n) * n ) by POLYEQ_5:2;
powersFS ((- (n + 1)),3,((2 * (n + 1)) - 1)) = (<*((- n) to_power 3)*> ^ (powersFS ((- n),3,((2 * n) - 1)))) ^ <*(n to_power 3)*> by Th48;
hence Sum (powersFS ((- (n + 1)),3,((2 * (n + 1)) - 1))) = ((- n) to_power 3) + (n to_power 3) by A3, A4, RVSUM_1:74
.= 0 by A5 ;
:: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A1, A2);
hence Sum (powersFS ((- k),3,((2 * k) - 1))) = 0 ; :: thesis: verum