let n be positive Nat; :: thesis: ex x being Integer ex y being Nat st Sum (powersFS (x,3,n)) = y |^ 3

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: ex x being Integer ex y being Nat st Sum (powersFS (x,3,n)) = y |^ 3

then consider k being Nat such that
A1: n = 2 * k ;
take - k ; :: thesis: ex y being Nat st Sum (powersFS ((- k),3,n)) = y |^ 3
take k ; :: thesis: Sum (powersFS ((- k),3,n)) = k |^ 3
thus Sum (powersFS ((- k),3,n)) = k |^ 3 by A1, Th49; :: thesis: verum

end;

suppose n is odd ; :: thesis: ex x being Integer ex y being Nat st Sum (powersFS (x,3,n)) = y |^ 3

then consider k being Nat such that
A2: n = (2 * k) + 1 by ABIAN:9;
take - (k + 1) ; :: thesis: ex y being Nat st Sum (powersFS ((- (k + 1)),3,n)) = y |^ 3
take 0 ; :: thesis: Sum (powersFS ((- (k + 1)),3,n)) = 0 |^ 3
n = (2 * (k + 1)) - 1 by A2;
hence Sum (powersFS ((- (k + 1)),3,n)) = 0 |^ 3 by Th50; :: thesis: verum

end;

end;