for S being feasible ManySortedSign
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 )