let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty MSAlgebra over S1
for C2 being non-empty MSAlgebra over 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 over S1
for C2 being non-empty MSAlgebra over 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 over S1; :: thesis: for C2 being non-empty MSAlgebra over 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 over 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 Th36; :: 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;
hence ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) ; :: thesis: verum

end;

assume that
A2: f is one-to-one and
A3: g is one-to-one and
A4: f,g form_morphism_between S1,S2 and
A5: f " ,g " form_morphism_between S2,S1 and
A6: the Sorts of C1 = the Sorts of C2 * f and
A7: 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, A4, A6, A7; :: 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, A3; :: 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 A5; :: 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 A5;
then rng f = the carrier of S2 by A2, FUNCT_1:33;
then f * (f ") = id the carrier of S2 by A2, FUNCT_1:39
.= id (dom the Sorts of C2) by PARTFUN1:def 2 ;
hence the Sorts of C2 = the Sorts of C2 * (f * (f ")) by RELAT_1:52
.= the Sorts of C1 * (f ") by A6, RELAT_1:36 ;
:: thesis: the Charact of C2 = the Charact of C1 * (g ")
dom (g ") = the carrier' of S2 by A5;
then rng g = the carrier' of S2 by A3, FUNCT_1:33;
then g * (g ") = id the carrier' of S2 by A3, FUNCT_1:39
.= id (dom the Charact of C2) by PARTFUN1:def 2 ;
hence the Charact of C2 = the Charact of C2 * (g * (g ")) by RELAT_1:52
.= the Charact of C1 * (g ") by A7, RELAT_1:36 ;
:: thesis: verum