let S be feasible ManySortedSign ; :: thesis: S is Subsignature of S
thus id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; :: according to INSTALG1:def 2 :: thesis: verum