let S be feasible ManySortedSign ; :: thesis: for T being Subsignature of S holds
( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
let T be Subsignature of S; :: thesis: ( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )
set f = id the carrier of T;
set g = id the carrier' of T;
A1: id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2;
the ResultSort of T = (id the carrier of T) * the ResultSort of T by FUNCT_2:23
.= the ResultSort of S * (id the carrier' of T) by A1, PUA2MSS1:def 13 ;
hence the ResultSort of T c= the ResultSort of S by RELAT_1:76; :: thesis: the Arity of T c= the Arity of S
A2: ( dom the Arity of T = the carrier' of T & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1;
then A3: dom the Arity of T c= dom the Arity of S by Th11;

now

let x be set ; :: thesis: ( x in dom the Arity of T implies the Arity of T . x = the Arity of S . x )
assume A4: x in dom the Arity of T ; :: thesis: the Arity of T . x = the Arity of S . x
then ( the Arity of T . x in rng the Arity of T & rng the Arity of T c= the carrier of T * ) by FUNCT_1:def 5, RELAT_1:def 19;
then reconsider p = the Arity of T . x as Element of the carrier of T * ;
(id the carrier' of T) . x = x by A2, A4, FUNCT_1:34;
then ( rng p c= the carrier of T & (id the carrier of T) * p = the Arity of S . x ) by A1, A2, A4, FINSEQ_1:def 4, PUA2MSS1:def 13;
hence the Arity of T . x = the Arity of S . x by RELAT_1:79; :: thesis: verum

end;

hence the Arity of T c= the Arity of S by A3, GRFUNC_1:8; :: thesis: verum