theorem Th3: :: CIRCUIT2:3

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 x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]