for S1, S2 being non empty non void Circuit-like ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for v1 being Vertex of S1 st v1 in InnerVertices S1 holds
for v2 being Vertex of S2 st v2 = f . v1 holds
action_at v2 = g . (action_at v1)