:: deftheorem Def8 defines the_value_of YELLOW_6:def 8 :
for T being non empty 1-sorted
for N being NetStr over T st N is constant & not N is empty holds
the_value_of N = the_value_of the mapping of N;