let S be non empty ManySortedSign ; :: thesis: for C being non-empty MSAlgebra of S holds C,C are_similar_wrt id the carrier of S, id the carrier' of S
let C be non-empty MSAlgebra of S; :: thesis: C,C are_similar_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;
A1: (id the carrier of S) " = id the carrier of S by FUNCT_1:67;
(id the carrier' of S) " = id the carrier' of S by FUNCT_1:67;
hence ( id the carrier of S, id the carrier' of S form_embedding_of C,C & (id the carrier of S) " ,(id the carrier' of S) " form_embedding_of C,C ) by A1, Th35; :: according to CIRCTRM1:def 13 :: thesis: verum