:: deftheorem defines OperMap CIRCTRM1:def 18 :
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 non empty Subset of (S -Terms V)
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st C calculates X,A holds
for f being SortMap of X,A,C
for b₈ being one-to-one Function holds
( b₈ is OperMap of X,A,C,f iff f,b₈ form_embedding_of X -Circuit A,C );