let a be Element of A0; :: thesis: a is DecoratedTree-like
consider x being object such that
A1: ( x in dom the Sorts of A0 & a in the Sorts of A0 . x ) by CARD_5:2;
reconsider x = x as SortSymbol of S by A1;
the Sorts of A0 is ManySortedSubset of the Sorts of (Free (S,X)) by Def6;
then the Sorts of A0 . x c= the Sorts of (Free (S,X)) . x by PBOOLE:def 2, PBOOLE:def 18;
then a is Element of the Sorts of (Free (S,X)) . x by A1;
hence a is DecoratedTree-like ; :: thesis: verum