let e be Element of the Sorts of (FreeMSA X) . v; :: thesis: ( e is finite & not e is empty & e is Function-like & e is Relation-like )
reconsider e9 = e as DecoratedTree by Th7;
thus e is finite by Th7; :: thesis: ( not e is empty & e is Function-like & e is Relation-like )
dom e9 is Tree ;
hence not e is empty ; :: thesis: ( e is Function-like & e is Relation-like )
thus ( e is Function-like & e is Relation-like ) by Th7; :: thesis: verum