let S, T be feasible ManySortedSign ; :: thesis: ( the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T implies T is Subsignature of S )
assume A1: the carrier of T c= the carrier of S ; :: thesis: ( not the Arity of T = the Arity of S | the carrier' of T or not the ResultSort of T = the ResultSort of S | the carrier' of T or T is Subsignature of S )
assume ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) ; :: thesis: T is Subsignature of S
then ( the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S ) by RELAT_1:88;
hence T is Subsignature of S by A1, Th14; :: thesis: verum