let S be feasible ManySortedSign ; :: thesis: for T being Subsignature of S holds

( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )

let T be Subsignature of S; :: thesis: ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )

A1: the Arity of T c= the Arity of S by Th11;

( the carrier of T = {} implies the carrier' of T = {} ) by Def1;

then A2: dom the ResultSort of T = the carrier' of T by FUNCT_2:def 1;

( dom the Arity of T = the carrier' of T & the ResultSort of T c= the ResultSort of S ) by Th11, FUNCT_2:def 1;

hence ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) by A2, A1, GRFUNC_1:23; :: thesis: verum

( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )

let T be Subsignature of S; :: thesis: ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )

A1: the Arity of T c= the Arity of S by Th11;

( the carrier of T = {} implies the carrier' of T = {} ) by Def1;

then A2: dom the ResultSort of T = the carrier' of T by FUNCT_2:def 1;

( dom the Arity of T = the carrier' of T & the ResultSort of T c= the ResultSort of S ) by Th11, FUNCT_2:def 1;

hence ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) by A2, A1, GRFUNC_1:23; :: thesis: verum