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 f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let f, g be Function; :: thesis: 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
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 implies for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1) )
assume that
f is one-to-one and
g is one-to-one and
A1: f,g form_morphism_between G1,G2 and
the Sorts of C1 = the Sorts of C2 * f and
A2: the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def 12 :: thesis: for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let o1 be Gate of G1; :: thesis: for o2 being Gate of G2 st o2 = g . o1 holds
Den (o2,C2) = Den (o1,C1)
let o2 be Gate of G2; :: thesis: ( o2 = g . o1 implies Den (o2,C2) = Den (o1,C1) )
assume A3: o2 = g . o1 ; :: thesis: Den (o2,C2) = Den (o1,C1)
dom g = the carrier' of G1 by A1;
hence Den (o2,C2) = Den (o1,C1) by A2, A3, FUNCT_1:13; :: thesis: verum