let L be non empty 1-sorted ; :: thesis: for N being net of L
for p being Function of N,N holds N * p is net of L
let N be net of L; :: thesis: for p being Function of N,N holds N * p is net of L
let p be Function of N,N; :: thesis: N * p is net of L
N * p = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * p) #) by Th7;
hence N * p is net of L ; :: thesis: verum