:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :
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) );