:: deftheorem Def8 defines * WAYBEL_9:def 8 :
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T
for N being NetStr over S
for b₅ being strict NetStr over T holds
( b₅ = f * N iff ( RelStr(# the carrier of b₅, the InternalRel of b₅ #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b₅ = f * the mapping of N ) );