let G1, G2 be non empty non void Circuit-like ManySortedSign ; 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; 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; 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; ( 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
; CIRCTRM1:def 13 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; for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )
let s2 be State of C2; ( 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; verum