take S ; :: thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S
thus id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; :: thesis: verum