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 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
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 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
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 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
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 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) )
assume A1:
C1,C2 are_similar_wrt f,g
; for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
then A2:
C2,C1 are_similar_wrt f " ,g "
by Th39;
let s1 be State of C1; for s2 being State of C2 st s1 = s2 * f holds
for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let s2 be State of C2; ( s1 = s2 * f implies for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) )
assume A3:
s1 = s2 * f
; for v1 being Vertex of G1 holds
( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
let v1 be Vertex of G1; ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 )
A4:
G1,G2 are_equivalent_wrt f,g
by A1, Th37;
then A5:
f,g form_morphism_between G1,G2
;
A6:
f " ,g " form_morphism_between G2,G1
by A4;
A7:
dom f = the carrier of G1
by A5;
A8:
dom (f ") = the carrier of G2
by A6;
reconsider v2 = f . v1 as Vertex of G2 by A5, Th30;
f is one-to-one
by A4;
then A9:
v1 = (f ") . v2
by A7, FUNCT_1:34;
thus
( s1 is_stable_at v1 implies s2 is_stable_at f . v1 )
( s2 is_stable_at f . v1 implies s1 is_stable_at v1 )proof
assume A10:
for
n being
Nat holds
(Following (s1,n)) . v1 = s1 . v1
;
FACIRC_1:def 9 s2 is_stable_at f . v1
let n be
Nat;
FACIRC_1:def 9 (Following (s2,n)) . (f . v1) = s2 . (f . v1)
n in NAT
by ORDINAL1:def 12;
then
Following (
s1,
n)
= (Following (s2,n)) * f
by A1, A3, Th55;
hence (Following (s2,n)) . (f . v1) =
(Following (s1,n)) . v1
by A7, FUNCT_1:13
.=
s1 . v1
by A10
.=
s2 . (f . v1)
by A3, A7, FUNCT_1:13
;
verum
end;
assume A11:
for n being Nat holds (Following (s2,n)) . (f . v1) = s2 . (f . v1)
; FACIRC_1:def 9 s1 is_stable_at v1
let n be Nat; FACIRC_1:def 9 (Following (s1,n)) . v1 = s1 . v1
A12:
n in NAT
by ORDINAL1:def 12;
s2 = s1 * (f ")
by A1, A3, Th51;
then
Following (s2,n) = (Following (s1,n)) * (f ")
by A2, A12, Th55;
hence (Following (s1,n)) . v1 =
(Following (s2,n)) . v2
by A8, A9, FUNCT_1:13
.=
s2 . v2
by A11
.=
s1 . v1
by A3, A7, FUNCT_1:13
;
verum