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;