:: deftheorem Def3 defines the_action_of CIRCTRM1:def 3 :
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) st X is SetWithCompoundTerm of S,V holds
for o being Gate of (X -CircuitStr)
for A being MSAlgebra over S
for b₆ being Function holds
( b₆ = the_action_of (o,A) iff for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
b₆ = the Charact of A . ((o9 . {}) `1) );