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

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