set G = DTConOSA X;
set D = bool [:(TS (DTConOSA X)),the carrier of S:];
deffunc H₁( Symbol of ) -> Subset of = @ $1;
deffunc H₂( Symbol of , set , FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:]) -> Subset of = @ $1,$3;
thus ex f being Function of TS (DTConOSA X), bool [:(TS (DTConOSA X)),the carrier of S:] st
( ( for t being Symbol of st t in Terminals (DTConOSA X) holds
f . (root-tree t) = H₁(t) ) & ( for nt being Symbol of
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f . (nt -tree ts) = H₂(nt, roots ts,f * ts) ) ) from DTCONSTR:sch 8(); :: thesis: verum