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

proof

set f = powersFS ((- 0),3,(2 * 0));
len (powersFS ((- 0),3,(2 * 0))) = 0 by Def7;
then powersFS ((- 0),3,(2 * 0)) = {} ;
hence Sum (powersFS ((- 0),3,(2 * 0))) = 0 |^ 3 ; :: thesis: verum

end;

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

proof

let n be 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)));
set g = powersFS ((- n),3,(2 * n));
set a = (- n) to_power 3;
set b = (n + 1) to_power 3;
A4: Sum (<*((- n) to_power 3)*> ^ (powersFS ((- n),3,(2 * n)))) = ((- n) to_power 3) + (Sum (powersFS ((- n),3,(2 * n)))) by RVSUM_1:76;
A5: ( n |^ 3 = (n * n) * n & (n + 1) |^ 3 = ((n + 1) * (n + 1)) * (n + 1) & (- n) to_power 3 = ((- n) * (- n)) * (- n) & (n + 1) to_power 3 = ((n + 1) * (n + 1)) * (n + 1) ) by POLYEQ_5:2;
powersFS ((- (n + 1)),3,(2 * (n + 1))) = (<*((- n) to_power 3)*> ^ (powersFS ((- n),3,(2 * n)))) ^ <*((n + 1) to_power 3)*> by Th47;
hence Sum (powersFS ((- (n + 1)),3,(2 * (n + 1)))) = (Sum (<*((- n) to_power 3)*> ^ (powersFS ((- n),3,(2 * n))))) + ((n + 1) to_power 3) by RVSUM_1:74
.= (n + 1) |^ 3 by A3, A4, A5 ;
:: thesis: verum

end;

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