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 holds
( dom f = the carrier of G1 & rng f c= the carrier of G2 & dom g = the carrier' of G1 & rng g c= the carrier' of G2 )