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

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

suppose S is empty ; :: 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 Lm1; :: thesis: verum

end;

suppose not S is empty ; :: 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 Lm2; :: thesis: verum

end;

end;