set f = id (Union the Sorts of (Free S,X));
( 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) ) by RELAT_1:71;
then reconsider f = id (Union the Sorts of (Free S,X)) as UnOp of (Union the Sorts of (Free S,X)) by FUNCT_2:4;
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 Lem'id; :: thesis: verum