:: deftheorem Def3 defines .incSubset LEXBFS:def 4 :
for F being natural-valued Function
for S being set
for k being Nat
for b₄ being natural-valued Function holds
( b₄ = F .incSubset (S,k) iff ( dom b₄ = dom F & ( for y being object holds
( ( y in S & y in dom F implies b₄ . y = (F . y) + k ) & ( not y in S implies b₄ . y = F . y ) ) ) ) );