:: deftheorem defines action_at MSAFREE2:def 7 :
for IIG being non empty non void Circuit-like ManySortedSign
for v being Vertex of IIG st v in InnerVertices IIG holds
for b₃ being OperSymbol of IIG holds
( b₃ = action_at v iff the_result_sort_of b₃ = v );