begin
Lm1:
1 = succ {}
;
scheme
OmegaInd{
F1()
-> Nat,
P1[
set ] } :
provided
A1:
P1[
{} ]
and A2:
for
a being
Nat st
P1[
a] holds
P1[
succ a]
scheme
RecUn{
F1()
-> set ,
F2()
-> Function,
F3()
-> Function,
P1[
set ,
set ,
set ] } :
provided
A1:
dom F2()
= omega
and A2:
F2()
. {} = F1()
and A3:
for
n being
Nat holds
P1[
n,
F2()
. n,
F2()
. (succ n)]
and A4:
dom F3()
= omega
and A5:
F3()
. {} = F1()
and A6:
for
n being
Nat holds
P1[
n,
F3()
. n,
F3()
. (succ n)]
and A7:
for
n being
Nat for
x,
y1,
y2 being
set st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2