for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)