:: deftheorem Def9 defines / MESFUNC1:def 8 :
for C being non empty set
for f being b₁ -defined ExtREAL -valued Function
for r being Real
for b₄ being PartFunc of C,ExtREAL holds
( b₄ = r / f iff ( dom b₄ = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b₄ holds
b₄ . c = r / (f . c) ) ) );