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 that
A2: the Arity of T = the Arity of S | the carrier' of T and
A3: the ResultSort of T = the ResultSort of S | the carrier' of T ; :: thesis: T is Subsignature of S
the Arity of T c= the Arity of S by A2, RELAT_1:59;
hence T is Subsignature of S by A1, A3, Th13, RELAT_1:59; :: thesis: verum