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) = ((m * a) + x) ^2
let k, x, m be Nat; :: thesis: ( (ArProg (b,a)) . k = x ^2 implies (ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) = ((m * a) + x) ^2 )
assume D2: (ArProg (b,a)) . k = x ^2 ; :: thesis: (ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) = ((m * a) + x) ^2
D1: (ArProg (b,a)) . k = (a * k) + b by NUMBER06:7;
set mm = m;
((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) = ((m * a) + x) ^2 by NUMBER06:7; :: thesis: verum