let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr over L
for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
let N be non empty NetStr over L; :: thesis: for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
let f be Function of N,N; :: thesis: N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
RelStr(# the carrier of (N * f), the InternalRel of (N * f) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2;
hence N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) by Def2; :: thesis: verum