theorem Th8: :: INSTALG1:8

for S being feasible ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S