:: deftheorem Def17 defines SortMap CIRCTRM1:def 17 :
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 b₇ being one-to-one Function holds
( b₇ is SortMap of X,A,C iff ( b₇ preserves_inputs_of X -CircuitStr ,G & ex g being Function st b₇,g form_embedding_of X -Circuit A,C ) );