for f being Element of F₁() holds P₁[f]

A1: P₁[ <*> NAT] and
A2: for f being Element of F₁() st P₁[f] holds
for n being Element of NAT st f ^ <*n*> in F₁() holds
P₁[f ^ <*n*>]