theorem Th2: :: CIRCUIT2:2

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e