A5
:
dom
F
_{5}
()
=
NAT
by
FUNCT_2:def 1
;
A6
:
dom
F
_{4}
()
=
NAT
by
FUNCT_2:def 1
;
thus
F
_{4}
()
=
F
_{5}
()
from
RECDEF_2:sch 6
(
A6
,
A1
,
A2
,
A5
,
A3
,
A4
);
:: thesis:
verum