:: deftheorem Def2 defines Subsignature INSTALG1:def 2 :
for S being feasible ManySortedSign
for b₂ being ManySortedSign holds
( b₂ is Subsignature of S iff id the carrier of b₂, id the carrier' of b₂ form_morphism_between b₂,S );