theorem Th5: :: CIRCUIT1:5

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k