:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 2 :
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)
for v being Vertex of (X -CircuitStr)
for A being MSAlgebra over S
for b₆ being set holds
( b₆ = the_sort_of (v,A) iff for u being Term of S,V st u = v holds
b₆ = the Sorts of A . (the_sort_of u) );