let a, b, c be Nat; (a + (b * c)) gcd b = a gcd b
defpred S1[ Nat] means (a + (b * $1)) gcd b = a gcd b;
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let kk be
Nat;
( S1[kk] implies S1[kk + 1] )
assume A2:
(a + (b * kk)) gcd b = a gcd b
;
S1[kk + 1]
hence
S1[
kk + 1]
;
verum
end;
A12:
S1[ 0 ]
;
for c being Nat holds S1[c]
from NAT_1:sch 2(A12, A1);
hence
(a + (b * c)) gcd b = a gcd b
; verum