reconsider M = N as non empty constant NetStr over T by A1;
set f = the mapping of M;
ex x being set st
( x in dom the mapping of M & the_value_of the mapping of M = the mapping of M . x ) by FUNCT_1:def 12;
then the_value_of the mapping of M in rng the mapping of M by FUNCT_1:def 3;
hence the_value_of the mapping of N is Element of T ; :: thesis: verum