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

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