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

A1: P₁[ {} ] and
A2: for t being Element of F₁()
for n being Nat st P₁[t] & t ^ <*n*> in F₁() holds
P₁[t ^ <*n*>]