:: deftheorem Def4 defines Swap HILB10_7:def 4 :
for f being Function
for a, b being object
for b₄ being Function holds
( b₄ = Swap (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) \ {a}) \/ {b} ) & ( not a in f . x implies b₄ . x = (f . x) \/ {a} ) ) ) ) );