let S be feasible ManySortedSign ; :: thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S

per cases ( S is void or not S is void ) ;

suppose S is void ; :: thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S

hence id the carrier of S, id the carrier' of S form_morphism_between S,S by MSALIMIT:6; :: thesis: verum

end;

suppose not S is void ; :: thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S

then reconsider S = S as non void feasible ManySortedSign ;
not S is empty ;
hence id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28; :: thesis: verum

end;

end;