:: deftheorem defines -Circuit CIRCTRM1:def 6 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being non-empty MSAlgebra over S holds X -Circuit A = MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #);