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

A1: for a being Ordinal
for n being non zero Nat holds P₁[n *^ (exp (omega,a))] and
A2: for a being Ordinal
for b being non empty Ordinal
for n being non zero Nat st P₁[b] & not a in rng (omega -exponent (CantorNF b)) holds
P₁[b (+) (n *^ (exp (omega,a)))]