A3: for k being Element of NAT st P₁[k] holds
P₁[k + 1] by A2;
let k be Nat; :: thesis: P₁[k]
A4: k is Element of NAT by ORDINAL1:def 12;
A5: P₁[ 0 ] by A1;
for k being Element of NAT holds P₁[k] from NAT_1:sch 1(A5, A3);
hence P₁[k] by A4; :: thesis: verum