let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
let f, g be Function; :: thesis: for C1 being non-empty MSAlgebra of S1
for C2 being non-empty MSAlgebra of S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
let C1 be non-empty MSAlgebra of S1; :: thesis: for C2 being non-empty MSAlgebra of S2 holds
( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )
let C2 be non-empty MSAlgebra of S2; :: thesis: ( C1,C2 are_similar_wrt f,g iff ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) )

hereby :: thesis: ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g implies C1,C2 are_similar_wrt f,g )

assume A1: C1,C2 are_similar_wrt f,g ; :: thesis: ( S1,S2 are_equivalent_wrt f,g & the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g )
hence S1,S2 are_equivalent_wrt f,g by Th37; :: thesis: ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g )
f,g form_embedding_of C1,C2 by A1, Def13;
hence ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) by Def12; :: thesis: verum

end;

assume that
A2: ( f is one-to-one & g is one-to-one ) and
A3: f,g form_morphism_between S1,S2 and
A4: f " ,g " form_morphism_between S2,S1 and
A5: ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) ; :: according to CIRCTRM1:def 9 :: thesis: C1,C2 are_similar_wrt f,g
thus ( 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 ) by A2, A3, A5; :: according to CIRCTRM1:def 12,CIRCTRM1:def 13 :: thesis: f " ,g " form_embedding_of C2,C1
thus ( f " is one-to-one & g " is one-to-one ) by A2; :: according to CIRCTRM1:def 12 :: thesis: ( f " ,g " form_morphism_between S2,S1 & the Sorts of C2 = the Sorts of C1 * (f " ) & the Charact of C2 = the Charact of C1 * (g " ) )
thus f " ,g " form_morphism_between S2,S1 by A4; :: thesis: ( the Sorts of C2 = the Sorts of C1 * (f " ) & the Charact of C2 = the Charact of C1 * (g " ) )
dom (f " ) = the carrier of S2 by A4, PUA2MSS1:def 13;
then rng f = the carrier of S2 by A2, FUNCT_1:55;
then f * (f " ) = id the carrier of S2 by A2, FUNCT_1:61
.= id (dom the Sorts of C2) by PARTFUN1:def 4 ;
hence the Sorts of C2 = the Sorts of C2 * (f * (f " )) by RELAT_1:78
.= the Sorts of C1 * (f " ) by A5, RELAT_1:55 ;
:: thesis: the Charact of C2 = the Charact of C1 * (g " )
dom (g " ) = the carrier' of S2 by A4, PUA2MSS1:def 13;
then rng g = the carrier' of S2 by A2, FUNCT_1:55;
then g * (g " ) = id the carrier' of S2 by A2, FUNCT_1:61
.= id (dom the Charact of C2) by PARTFUN1:def 4 ;
hence the Charact of C2 = the Charact of C2 * (g * (g " )) by RELAT_1:78
.= the Charact of C1 * (g " ) by A5, RELAT_1:55 ;
:: thesis: verum