for T being non empty 1-sorted
for N being net of T
for M being subnet of N
for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)