theorem :: INSTALG1:14

for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T holds
T is Subsignature of S