theorem Th47: :: CIRCTRM1:47

for G1, G2 being non empty non void Circuit-like ManySortedSign
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 n being Nat holds Following (s1,n) = (Following (s2,n)) * f