:: deftheorem defines form_embedding_of CIRCTRM1:def 12 :
for S1, S2 being non empty ManySortedSign
for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over S2 holds
( f,g form_embedding_of C1,C2 iff ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) );