:: deftheorem Def1 defines \// WAYBEL_5:def 1 :
for L being non empty RelStr
for F being Function-yielding Function
for b₃ being Function of (dom F), the carrier of L holds
( b₃ = \// (F,L) iff for x being object st x in dom F holds
b₃ . x = \\/ ((F . x),L) );