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
A11: dom IT1 = dom F and
A12: 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
A13: dom IT2 = dom F and
A14: 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 A15: x in dom IT1 ; :: thesis: IT1 . b₁ = IT2 . b₁

per cases ( ( x in S & x in dom F ) or not x in S ) by A11, A15;

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

then IT1 . x = (F . x) + k by A12;
hence IT1 . x = IT2 . x by A14, A16; :: thesis: verum

end;

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

then IT1 . x = F . x by A12;
hence IT1 . x = IT2 . x by A14, A17; :: thesis: verum

end;

end;

end;

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