:: deftheorem Def3 defines <- FINSEQ_4:def 3 :
for f being Function
for y being object st f just_once_values y holds
for b₃ being set holds
( b₃ = f <- y iff ( b₃ in dom f & f . b₃ = y ) );