theorem Th7: :: CIRCUIT1:7

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
for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]