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 A1: ( f,g form_embedding_of C1,C2 & 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 " ) )
then A2: ( f is one-to-one & f " is one-to-one ) by Def12;
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, Def12;
then A3: ( dom f = the carrier of G1 & dom s1 = the carrier of G1 ) by CIRCUIT1:4, PUA2MSS1:def 13;
A4: (s1 * (f " )) * f = s1 * ((f " ) * f) by RELAT_1:55
.= s1 * (id (dom f)) by A2, FUNCT_1:61
.= s1 by A3, RELAT_1:78 ;
f " ,g " form_morphism_between G2,G1 by A1, Def12;
then A5: ( dom (f " ) = the carrier of G2 & dom s2 = the carrier of G2 ) by CIRCUIT1:4, PUA2MSS1:def 13;
(s2 * f) * (f " ) = s2 * (f * (f " )) by RELAT_1:55
.= s2 * (((f " ) " ) * (f " )) by A2, FUNCT_1:65
.= s2 * (id (dom (f " ))) by A2, FUNCT_1:61 ;
hence ( s1 = s2 * f iff s2 = s1 * (f " ) ) by A4, A5, RELAT_1:78; :: thesis: verum