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 )
;

end;

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;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