:: deftheorem Def1 defines |[ BROUWER3:def 1 :
for f being real-valued Function
for b₂ being Function holds
( b₂ = |[f]| iff ( dom b₂ = dom f & ( for x being object st x in dom b₂ holds
b₂ . x = |[(f . x)]| ) ) );