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