let G2, G1 be non empty non void Circuit-like ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty Circuit of non-empty
for C2 being non-empty Circuit of non-empty st f,g form_embedding_of C1,C2 holds
for s2 being State of
for s1 being State of st s1 = s2 * f & ( for v being Vertex of 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 non-empty
for C2 being non-empty Circuit of non-empty st f,g form_embedding_of C1,C2 holds
for s2 being State of
for s1 being State of st s1 = s2 * f & ( for v being Vertex of 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 non-empty ; :: thesis: for C2 being non-empty Circuit of non-empty st f,g form_embedding_of C1,C2 holds
for s2 being State of
for s1 being State of st s1 = s2 * f & ( for v being Vertex of 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 non-empty ; :: thesis: ( f,g form_embedding_of C1,C2 implies for s2 being State of
for s1 being State of st s1 = s2 * f & ( for v being Vertex of 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
for s1 being State of st s1 = s2 * f & ( for v being Vertex of 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 ; :: thesis: for s1 being State of st s1 = s2 * f & ( for v being Vertex of st v in InputVertices G1 holds
s2 is_stable_at f . v ) holds
Following s1 = (Following s2) * f
let s1 be State of ; :: thesis: ( s1 = s2 * f & ( for v being Vertex of 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 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 by A1, Th45;
A5: dom f = the carrier of G1 by A2, PUA2MSS1:def 13;

now

let v be Vertex of ; :: 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 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 A7: s2 is_stable_at f . v by A4;
Following s2,1 = Following s2 by FACIRC_1:14;
hence s2' . v = s2 . (f . v) by A6, A7, FACIRC_1:def 9
.= s1 . v by A3, A5, FUNCT_1:23 ;
:: thesis: verum

end;

A8: f .: (InnerVertices G1) c= InnerVertices G2 by A2, Th33;
assume A9: v in InnerVertices G1 ; :: thesis: s2' . 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 12;
A11: action_at fv = g . (action_at v) by A2, A9, Th34;
thus s2' . 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, Th43
.= (Den (action_at v),C1) . ((action_at v) depends_on_in s1) by A1, A3, A11, Th44 ; :: thesis: verum

end;

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