let G1, G2 be 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
for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let f, g be 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
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let C1 be 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
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let C2 be non-empty Circuit of G2; ( 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
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1 )
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
the Charact of C1 = the Charact of C2 * g
; CIRCTRM1:def 12 for o1 being Gate of G1
for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let o1 be Gate of G1; for o2 being Gate of G2 st o2 = g . o1 holds
for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let o2 be Gate of G2; ( o2 = g . o1 implies for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1 )
assume A2:
o2 = g . o1
; for s1 being State of C1
for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let s1 be State of C1; for s2 being State of C2 st s1 = s2 * f holds
o2 depends_on_in s2 = o1 depends_on_in s1
let s2 be State of C2; ( s1 = s2 * f implies o2 depends_on_in s2 = o1 depends_on_in s1 )
assume A3:
s1 = s2 * f
; o2 depends_on_in s2 = o1 depends_on_in s1
thus o2 depends_on_in s2 =
s2 * (the_arity_of o2)
by CIRCUIT1:def 3
.=
s2 * (f * (the_arity_of o1))
by A1, A2
.=
s1 * (the_arity_of o1)
by A3, RELAT_1:36
.=
o1 depends_on_in s1
by CIRCUIT1:def 3
; verum