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 s being State of C2 holds s * f is State of C1
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 s being State of C2 holds s * f is State of C1
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 s being State of C2 holds s * f is State of C1
let C2 be non-empty Circuit of G2; :: thesis: ( C1,C2 are_similar_wrt f,g implies for s being State of C2 holds s * f is State of C1 )
assume f,g form_embedding_of C1,C2 ; :: according to CIRCTRM1:def 13 :: thesis: ( not f " ,g " form_embedding_of C2,C1 or for s being State of C2 holds s * f is State of C1 )
hence ( not f " ,g " form_embedding_of C2,C1 or for s being State of C2 holds s * f is State of C1 ) by Th45; :: thesis: verum