scheme :: NUMBER17:sch 3
STEP3{ P₁[ Nat] } :

for k being Nat holds P₁[k]

provided

A1: for k being Nat holds
( P₁[3 * k] & P₁[(3 * k) + 1] & P₁[(3 * k) + 2] )