let G1, G2 be non empty non void Circuit-like ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let f, g be Function; :: thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let C2 be non-empty Circuit of G2; :: thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") ) )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f " ,g " form_embedding_of C2,C1 ; :: according to CIRCTRM1:def 13 :: thesis: for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
A3: f is one-to-one by A1;
let s1 be State of C1; :: thesis: for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let s2 be State of C2; :: thesis: ( s1 = s2 * f iff s2 = s1 * (f ") )
f,g form_morphism_between G1,G2 by A1;
then A4: dom f = the carrier of G1 ;
A5: dom s1 = the carrier of G1 by CIRCUIT1:3;
A6: (s1 * (f ")) * f = s1 * ((f ") * f) by RELAT_1:36
.= s1 * (id (dom f)) by A3, FUNCT_1:39
.= s1 by A4, A5, RELAT_1:52 ;
f " ,g " form_morphism_between G2,G1 by A2;
then A7: dom (f ") = the carrier of G2 ;
A8: dom s2 = the carrier of G2 by CIRCUIT1:3;
(s2 * f) * (f ") = s2 * (f * (f ")) by RELAT_1:36
.= s2 * (((f ") ") * (f ")) by A3, FUNCT_1:43
.= s2 * (id (dom (f "))) by A3, FUNCT_1:39 ;
hence ( s1 = s2 * f iff s2 = s1 * (f ") ) by A6, A7, A8, RELAT_1:52; :: thesis: verum