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 )
( the carrier of T = {} implies the carrier' of T = {} ) by Def1;
then ( dom the ResultSort of T = the carrier' of T & dom the Arity of T = the carrier' of T & the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S ) by Th12, 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 GRFUNC_1:64; :: thesis: verum