theorem :: CIRCUIT1:16

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)