let IT1, IT2 be natural-valued Function; :: thesis: ( dom IT1 = dom F & ( for y being object 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 object 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 object 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 object 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

( ( 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 object 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 object 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 object 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 :: thesis: for x being object st x in dom IT1 holds

IT1 . x = IT2 . x

hence
IT1 = IT2
by A11, A13, FUNCT_1:2; :: thesis: verumIT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . b_{1} = IT2 . b_{1} )

assume A15: x in dom IT1 ; :: thesis: IT1 . b_{1} = IT2 . b_{1}

end;assume A15: x in dom IT1 ; :: thesis: IT1 . b