scheme :: ORDINAL2:sch 17
OmegaInd{ F1() -> Nat, P1[ object ] } :
P1[F1()]
provided
A1: P1[ 0 ] and
A2: for a being Nat st P1[a] holds
P1[ succ a]