let T be non empty 1-sorted ; :: thesis: 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)
let N be net of T; :: thesis: 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)
let M be subnet of N; :: thesis: for e being Embedding of M,N
for i being Element of M holds M . i = N . (e . i)
let e be Embedding of M,N; :: thesis: for i being Element of M holds M . i = N . (e . i)
let i be Element of M; :: thesis: M . i = N . (e . i)
the mapping of M = the mapping of N * e by Def3;
hence M . i = N . (e . i) by FUNCT_2:15; :: thesis: verum