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 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
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 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
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 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f )
assume A1: f,g form_embedding_of C1,C2 ; :: thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
then A2: f,g form_morphism_between G1,G2 ;
let s2 be State of C2; :: thesis: for s1 being State of C1 st s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let s1 be State of C1; :: thesis: ( s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ) implies Following s1 = (Following s2) * f )
assume that
A3: s1 = s2 * f and
A4: for v being Vertex of G1 st v in InputVertices G1 holds
s2 is_stable_at f . v ; :: thesis: Following s1 = (Following s2) * f
reconsider s29 = (Following s2) * f as State of C1 by A1, Th44;
A5: dom f = the carrier of G1 by A2;

now :: thesis: for v being Vertex of G1 holds
( ( v in InputVertices G1 implies s29 . v = s1 . v ) & ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) ) )

let v be Vertex of G1; :: thesis: ( ( v in InputVertices G1 implies s29 . v = s1 . v ) & ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) ) )
A6: s29 . v = (Following s2) . (f . v) by A5, FUNCT_1:13;
reconsider fv = f . v as Vertex of G2 by A2, Th30;

hereby :: thesis: ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) )

assume v in InputVertices G1 ; :: thesis: s29 . v = s1 . v
then A7: s2 is_stable_at f . v by A4;
Following (s2,1) = Following s2 by FACIRC_1:14;
hence s29 . v = s2 . (f . v) by A6, A7
.= s1 . v by A3, A5, FUNCT_1:13 ;
:: thesis: verum

end;

A8: f .: (InnerVertices G1) c= InnerVertices G2 by A2, Th32;
assume A9: v in InnerVertices G1 ; :: thesis: s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1)
then A10: fv in f .: (InnerVertices G1) by A5, FUNCT_1:def 6;
A11: action_at fv = g . (action_at v) by A2, A9, Th33;
thus s29 . v = (Den ((action_at fv),C2)) . ((action_at fv) depends_on_in s2) by A6, A8, A10, CIRCUIT2:def 5
.= (Den ((action_at v),C1)) . ((action_at fv) depends_on_in s2) by A1, A11, Th42
.= (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) by A1, A3, A11, Th43 ; :: thesis: verum

end;

hence Following s1 = (Following s2) * f by CIRCUIT2:def 5; :: thesis: verum