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