theorem Th51: :: CIRCTRM1:51

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 C1,C2 are_similar_wrt f,g holds
for s1 being State of C1
for s2 being State of C2 holds
( s1 = s2 * f iff s2 = s1 * (f ") )