:: deftheorem Def3 defines *' WAYBEL32:def 3 :
for S being non empty 1-sorted
for R being non empty RelStr
for f being Function of the carrier of R, the carrier of S
for b₄ being non empty strict NetStr over S holds
( b₄ = R *' f iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b₄ = f ) );