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

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