for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG holds
( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )