let a, b be positive Nat; :: thesis: for k, x, m being Nat st (ArProg (b,a)) . k = x ^2 holds
(ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) is square
let k, x, m be Nat; :: thesis: ( (ArProg (b,a)) . k = x ^2 implies (ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) is square )
assume D2: (ArProg (b,a)) . k = x ^2 ; :: thesis: (ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) is square
D1: (ArProg (b,a)) . k = b + (a * k) by NUMBER06:7;
((m * a) + x) ^2 = (((m * a) ^2) + (((2 * m) * a) * x)) + (x ^2)
.= (a * ((((m ^2) * a) + ((2 * m) * x)) + k)) + b by D1, D2 ;
hence (ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) is square by NUMBER06:7; :: thesis: verum