let S be non empty ManySortedSign ; :: thesis: for C being non-empty MSAlgebra over S holds id the carrier of S, id the carrier' of S form_embedding_of C,C
let C be non-empty MSAlgebra over S; :: thesis: id the carrier of S, id the carrier' of S form_embedding_of C,C
thus id the carrier of S is one-to-one ; :: according to CIRCTRM1:def 12 :: 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 & the Sorts of C = the Sorts of C * (id the carrier of S) & the Charact of C = the Charact of C * (id the carrier' of S) )
A1: dom the Sorts of C = the carrier of S by PARTFUN1:def 2;
dom the Charact of C = the carrier' of S by PARTFUN1:def 2;
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 & the Sorts of C = the Sorts of C * (id the carrier of S) & the Charact of C = the Charact of C * (id the carrier' of S) ) by A1, INSTALG1:8, RELAT_1:52; :: thesis: verum