scheme :: ORDINAL7:sch 3
OrdinalCNFIndC{ P₁[ non empty Ordinal] } :

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

provided

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))]