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, Def12;
then A5: dom f = the carrier of G1 by PUA2MSS1:def 13;
reconsider v2 = f . v1 as Vertex of G2 by A4, Th31;
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)
n in NAT by ORDINAL1:def 13;
then Following s1,n = (Following s2,n) * f by A1, A2, A3, Th48;
hence (Following s2,n) . (f . v1) = (Following s1,n) . v1 by A5, FUNCT_1:23
.= s1 . v1 by A6
.= s2 . (f . v1) by A3, A5, FUNCT_1:23 ;
:: 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
n in NAT by ORDINAL1:def 13;
then Following s1,n = (Following s2,n) * f by A1, A2, A3, Th48;
hence (Following s1,n) . v1 = (Following s2,n) . v2 by A5, FUNCT_1:23
.= s2 . v2 by A7
.= s1 . v1 by A3, A5, FUNCT_1:23 ;
:: thesis: verum