:: deftheorem defines sequence_to_net CARDFIL2:def 29 :
for L being 1-sorted
for s being sequence of the carrier of L holds sequence_to_net s = NetStr(# NAT,NATOrd,s #);