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 f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 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 f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 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 f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 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: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 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 that
A1: f,g form_embedding_of C1,C2 and
A2: f preserves_inputs_of G1,G2 ; :: thesis: for s2 being State of C2
for s1 being State of C1 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: for s1 being State of C1 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 s1 be State of C1; :: 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: f,g form_morphism_between G1,G2 by A1;
then A5: dom f = the carrier of G1 ;
reconsider v2 = f . v1 as Vertex of G2 by A4, Th30;
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 A6: 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)
Following (s1,n) = (Following (s2,n)) * f by A1, A2, A3, Th47;
hence (Following (s2,n)) . (f . v1) = (Following (s1,n)) . v1 by A5, FUNCT_1:13
.= s1 . v1 by A6
.= s2 . (f . v1) by A3, A5, FUNCT_1:13 ;
:: thesis: verum

end;

assume A7: 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
Following (s1,n) = (Following (s2,n)) * f by A1, A2, A3, Th47;
hence (Following (s1,n)) . v1 = (Following (s2,n)) . v2 by A5, FUNCT_1:13
.= s2 . v2 by A7
.= s1 . v1 by A3, A5, FUNCT_1:13 ;
:: thesis: verum