theorem :: MSALIMIT:6

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