let a, b be Nat; :: thesis: for t being Integer st b |^ 2 = ((2 * a) + t) * t holds

ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

let t be Integer; :: thesis: ( b |^ 2 = ((2 * a) + t) * t implies ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 )

assume b |^ 2 = ((2 * a) + t) * t ; :: thesis: ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

then A1: b |^ 2 = ((a + t) + a) * ((a + t) - a)

.= ((a + t) |^ 2) - (a |^ 2) by NEWTON01:1 ;

|.(a + t).| in NAT by INT_1:3;

then consider c being Nat such that

A2: c = |.(a + t).| ;

( c |^ 2 = (a + t) |^ 2 or c |^ 2 = (- (a + t)) |^ 2 ) by A2, ABSVALUE:1;

then c |^ 2 = (a + t) |^ 2 by WSIERP_1:1;

hence ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 by A1; :: thesis: verum

ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

let t be Integer; :: thesis: ( b |^ 2 = ((2 * a) + t) * t implies ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 )

assume b |^ 2 = ((2 * a) + t) * t ; :: thesis: ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

then A1: b |^ 2 = ((a + t) + a) * ((a + t) - a)

.= ((a + t) |^ 2) - (a |^ 2) by NEWTON01:1 ;

|.(a + t).| in NAT by INT_1:3;

then consider c being Nat such that

A2: c = |.(a + t).| ;

( c |^ 2 = (a + t) |^ 2 or c |^ 2 = (- (a + t)) |^ 2 ) by A2, ABSVALUE:1;

then c |^ 2 = (a + t) |^ 2 by WSIERP_1:1;

hence ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 by A1; :: thesis: verum