defpred S₂[ DecoratedTree of the carrier of PeanoNat] means $1 = NAT-to-PN . (PN-to-NAT . $1);

A1: now :: thesis:

let s be Symbol of PeanoNat; :: thesis:
assume A2: s in Terminals PeanoNat ; :: thesis:
then NAT-to-PN . (PN-to-NAT . (root-tree s)) = NAT-to-PN . 0 by Def8
.= root-tree O by Def10 ;
hence S₂[ root-tree s] by A2, Lm10, TARSKI:def 1; :: thesis:

end;

A3: now :: thesis:

let nt be Symbol of PeanoNat; :: thesis:
let ts be FinSequence of TS PeanoNat; :: thesis:
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of PeanoNat st t in rng ts holds
S₂[t] ; :: thesis:
A6: nt <> O by A4, Lm8;
( roots ts = <*O*> or roots ts = <*S*> ) by A4, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider dt being Element of FinTrees the carrier of PeanoNat such that
A7: ts = <*dt*> and
A8: dt in TS PeanoNat by Th5;
reconsider dt = dt as Element of TS PeanoNat by A8;
rng ts = {dt} by A7, FINSEQ_1:38;
then dt in rng ts by TARSKI:def 1;
then A9: dt = NAT-to-PN . (PN-to-NAT . dt) by A5;
A10: PN-to-NAT * ts = <*(PN-to-NAT . dt)*> by A7, FINSEQ_2:35;
set N = PN-to-NAT . dt;
A11: plus-one <*(PN-to-NAT . dt)*> = (PN-to-NAT . dt) + 1 ;
NAT-to-PN . ((PN-to-NAT . dt) + 1) = PNsucc dt by A9, Def10
.= nt -tree ts by A6, A7, Lm2, TARSKI:def 2 ;
hence S₂[nt -tree ts] by A4, A10, A11, Def8; :: thesis:

end;

for t being DecoratedTree of the carrier of PeanoNat st t in TS PeanoNat holds
S₂[t] from DTCONSTR:sch 7(A1, A3);
hence for pn being Element of TS PeanoNat holds pn = NAT-to-PN . (PN-to-NAT . pn) ; :: thesis: