let a be Nat; :: thesis: ( a is odd implies ex b being Nat st (a |^ 2) + (b |^ 2) = (b + 1) |^ 2 )
assume a is odd ; :: thesis: ex b being Nat st (a |^ 2) + (b |^ 2) = (b + 1) |^ 2
then consider k being Nat such that
A2: a = (2 * k) + 1 by ABIAN:9;
(((2 * k) + 1) |^ 2) + (((2 * (k |^ 2)) + (2 * k)) |^ 2) = (((2 * (k |^ 2)) + (2 * k)) + 1) |^ 2 by Th2;
hence ex b being Nat st (a |^ 2) + (b |^ 2) = (b + 1) |^ 2 by A2; :: thesis: verum