let S be non empty ManySortedSign ; :: thesis: S,S are_equivalent_wrt id the carrier of S, id the carrier' of S
set f = id the carrier of S;
set g = id the carrier' of S;
thus id the carrier of S is one-to-one ; :: according to CIRCTRM1:def 9 :: thesis: ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & (id the carrier of S) " ,(id the carrier' of S) " form_morphism_between S,S )
A1: (id the carrier of S) " = id the carrier of S by FUNCT_1:45;
(id the carrier' of S) " = id the carrier' of S by FUNCT_1:45;
hence ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & (id the carrier of S) " ,(id the carrier' of S) " form_morphism_between S,S ) by A1, INSTALG1:8; :: thesis: verum