let G2, G1 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 by Def12;
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 s2' = (Following s2) * f as State of C1 by A1, Th45;
A5: ( dom f = the carrier of G1 & rng f c= the carrier of G2 ) by A2, PUA2MSS1:def 13;

now

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

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

assume v in InputVertices G1 ; :: thesis: s2' . v = s1 . v
then ( s2 is_stable_at f . v & Following s2,1 = Following s2 ) by A4, FACIRC_1:14;
hence s2' . v = s2 . (f . v) by A6, FACIRC_1:def 9
.= s1 . v by A3, A5, FUNCT_1:23 ;
:: thesis: verum

end;

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

end;

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