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
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 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f 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 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
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
Following s1 = (Following s2) * f )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f .: (InputVertices G1) c= InputVertices G2 ; :: according to CIRCTRM1:def 11 :: thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let s2 be State of C2; :: thesis: for s1 being State of C1 st s1 = s2 * f holds
Following s1 = (Following s2) * f
let s1 be State of C1; :: thesis: ( s1 = s2 * f implies Following s1 = (Following s2) * f )
assume A3: s1 = s2 * f ; :: thesis: Following s1 = (Following s2) * f
A4: dom f = the carrier of G1 by A1, Th42;

now

let v be Vertex of G1; :: thesis: ( v in InputVertices G1 implies s2 is_stable_at f . v )
assume v in InputVertices G1 ; :: thesis: s2 is_stable_at f . v
then f . v in f .: (InputVertices G1) by A4, FUNCT_1:def 12;
hence s2 is_stable_at f . v by A2, FACIRC_1:18; :: thesis: verum

end;

hence Following s1 = (Following s2) * f by A1, A3, Th46; :: thesis: verum