:: deftheorem Def5 defines Ext HILB10_7:def 5 :
for f being Function
for a, b being object
for b₄ being Function holds
( b₄ = Ext (f,a,b) iff ( dom b₄ = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies b₄ . x = (f . x) \/ {b} ) & ( not a in f . x implies b₄ . x = f . x ) ) ) ) );