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

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