for a being non empty Ordinal holds P₁[a]

A1: for a being Ordinal holds P₁[ exp (omega,a)] and
A2: for a being Ordinal
for b being non empty Ordinal st P₁[b] holds
P₁[b (+) (exp (omega,a))]