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 A1: ( f,g form_embedding_of C1,C2 & 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 A2: 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 )
A3: f,g form_morphism_between G1,G2 by A1, Def12;
then A4: dom f = the carrier of G1 by PUA2MSS1:def 13;
reconsider v2 = f . v1 as Vertex of G2 by A3, 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 A5: 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, Th48;
hence (Following s2,n) . (f . v1) = (Following s1,n) . v1 by A4, FUNCT_1:23
.= s1 . v1 by A5
.= s2 . (f . v1) by A2, A4, FUNCT_1:23 ;
:: thesis: verum

end;

assume A6: 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, Th48;
hence (Following s1,n) . v1 = (Following s2,n) . v2 by A4, FUNCT_1:23
.= s2 . v2 by A6
.= s1 . v1 by A2, A4, FUNCT_1:23 ;
:: thesis: verum