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 C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following s1,n = (Following s2,n) * f
let f, g be Function; :: thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following s1,n = (Following s2,n) * f
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following s1,n = (Following s2,n) * f
let C2 be non-empty Circuit of G2; :: thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following s1,n = (Following s2,n) * f )
assume A1: C1,C2 are_similar_wrt f,g ; :: thesis: for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following s1,n = (Following s2,n) * f
then f,g form_embedding_of C1,C2 by Def13;
hence for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
for n being Element of NAT holds Following s1,n = (Following s2,n) * f by A1, Th48, Th54; :: thesis: verum