let IT1, IT2 be natural-valued Function; :: thesis: ( dom IT1 = dom F & ( for y being set holds
( ( y in S & y in dom F implies IT1 . y = (F . y) + k ) & ( not y in S implies IT1 . y = F . y ) ) ) & dom IT2 = dom F & ( for y being set holds
( ( y in S & y in dom F implies IT2 . y = (F . y) + k ) & ( not y in S implies IT2 . y = F . y ) ) ) implies IT1 = IT2 )
assume that
A10: ( dom IT1 = dom F & ( for y being set holds
( ( y in S & y in dom F implies IT1 . y = (F . y) + k ) & ( not y in S implies IT1 . y = F . y ) ) ) ) and
A11: ( dom IT2 = dom F & ( for y being set holds
( ( y in S & y in dom F implies IT2 . y = (F . y) + k ) & ( not y in S implies IT2 . y = F . y ) ) ) ) ; :: thesis: IT1 = IT2

now

let x be set ; :: thesis: ( x in dom IT1 implies IT1 . b₁ = IT2 . b₁ )
assume A12: x in dom IT1 ; :: thesis: IT1 . b₁ = IT2 . b₁

per cases ( ( x in S & x in dom F ) or not x in S ) by A10, A12;

suppose ( x in S & x in dom F ) ; :: thesis: IT1 . b₁ = IT2 . b₁

then ( IT1 . x = (F . x) + k & IT2 . x = (F . x) + k ) by A10, A11;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

suppose not x in S ; :: thesis: IT1 . b₁ = IT2 . b₁

then ( IT1 . x = F . x & IT2 . x = F . x ) by A10, A11;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

end;

end;

hence IT1 = IT2 by A10, A11, FUNCT_1:9; :: thesis: verum