let it1, it2 be Function of (TS PeanoNat),NAT; :: thesis: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it1 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it1 . (nt -tree ts) = plus-one (it1 * ts) ) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it2 . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it2 . (nt -tree ts) = plus-one (it2 * ts) ) implies it1 = it2 )
assume that
A1: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it1 . (root-tree t) = H₁(t) ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it1 . (nt -tree ts) = H₃(nt, roots ts,it1 * ts) ) ) and
A2: ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
it2 . (root-tree t) = H₁(t) ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
it2 . (nt -tree ts) = H₃(nt, roots ts,it2 * ts) ) ) ; :: thesis: it1 = it2
thus it1 = it2 from DTCONSTR:sch 9(A1, A2); :: thesis: verum