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
f preserves_inputs_of G1,G2
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
f preserves_inputs_of G1,G2
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
f preserves_inputs_of G1,G2
let C2 be non-empty Circuit of G2; :: thesis: ( C1,C2 are_similar_wrt f,g implies f preserves_inputs_of G1,G2 )
assume C1,C2 are_similar_wrt f,g ; :: thesis: f preserves_inputs_of G1,G2
hence f .: (InputVertices G1) c= InputVertices G2 by Th53; :: according to CIRCTRM1:def 11 :: thesis: verum