:: deftheorem Def1 defines ExtendInt TOPALG_5:def 1 :
for r being Real
for b₂ being Function of I[01],R^1 holds
( b₂ = ExtendInt r iff for x being Point of I[01] holds b₂ . x = r * x );