:: deftheorem Def2 defines * WAYBEL28:def 2 :
for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N
for b₄ being non empty strict NetStr over L holds
( b₄ = N * f iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₄ = the mapping of N * f ) );