let S1, S2, S be non empty non void Circuit-like ManySortedSign ; :: thesis: ( S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2 )
assume A1: S = S1 +* S2 ; :: thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2
let A1 be non-empty Circuit of S1; :: thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2
let A2 be non-empty Circuit of S2; :: thesis: for A being non-empty Circuit of S
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2
let A be non-empty Circuit of S; :: thesis: for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2
let s be State of A; :: thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2
let s2 be State of A2; :: thesis: ( s2 = s | the carrier of S2 implies for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2 )
assume A2: s2 = s | the carrier of S2 ; :: thesis: for g being Gate of S
for g2 being Gate of S2 st g = g2 holds
g depends_on_in s = g2 depends_on_in s2
let o be OperSymbol of S; :: thesis: for g2 being Gate of S2 st o = g2 holds
o depends_on_in s = g2 depends_on_in s2
let o2 be OperSymbol of S2; :: thesis: ( o = o2 implies o depends_on_in s = o2 depends_on_in s2 )
assume A3: o = o2 ; :: thesis: o depends_on_in s = o2 depends_on_in s2
A4: the carrier of S2 |` (the_arity_of o2) = the_arity_of o2 ;
thus o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def 3
.= s * (the_arity_of o2) by A1, A3, Th14
.= s2 * (the_arity_of o2) by A2, A4, MONOID_1:1
.= o2 depends_on_in s2 by CIRCUIT1:def 3 ; :: thesis: verum