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 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; :: 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 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; :: 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 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ) :: thesis: ( 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 ; :: according to FACIRC_1:def 9 :: thesis: s2 is_stable_at f . v1
let n be Nat; :: according to FACIRC_1:def 9 :: thesis: (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 ;
:: thesis: verum

end;

assume A11: for n being Nat holds (Following (s2,n)) . (f . v1) = s2 . (f . v1) ; :: according to FACIRC_1:def 9 :: thesis: s1 is_stable_at v1
let n be Nat; :: according to FACIRC_1:def 9 :: thesis: (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 ;
:: thesis: verum