set f = id (Union the Sorts of (Free (S,X)));
A1: dom (id (Union the Sorts of (Free (S,X)))) = Union the Sorts of (Free (S,X)) ;
rng (id (Union the Sorts of (Free (S,X)))) = Union the Sorts of (Free (S,X)) ;
then reconsider f = id (Union the Sorts of (Free (S,X))) as UnOp of (Union the Sorts of (Free (S,X))) by A1, FUNCT_2:2;
take f ; :: thesis: for s being SortSymbol of S holds f .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s
thus for s being SortSymbol of S holds f .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s by Th4; :: thesis: verum