theorem Th13: :: INSTALG1:13

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