theorem :: CIRCTRM1:15

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for A being non-empty finite-yielding MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of (X -CircuitStr) holds Den (g,(X -Circuit A)) = the_action_of (g,A) by Def5;