:: deftheorem Def1 defines On MEASURE7:def 1 :
for S being non empty set
for H being Function of S,ExtREAL
for b₃ being sequence of ExtREAL holds
( b₃ = On H iff for n being Element of NAT holds
( ( n in S implies b₃ . n = H . n ) & ( not n in S implies b₃ . n = 0. ) ) );