let IT1, IT2 be Function; :: thesis: ( dom IT1 = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
IT1 . (m + k) = p . m ) & dom IT2 = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds
IT2 . (m + k) = p . m ) implies IT1 = IT2 )
assume that
A5: dom IT1 = { (m + k) where m is Nat : m in dom p } and
A6: for m being Nat st m in dom p holds
IT1 . (m + k) = p . m and
A7: dom IT2 = { (m + k) where m is Nat : m in dom p } and
A8: for m being Nat st m in dom p holds
IT2 . (m + k) = p . m ; :: thesis: IT1 = IT2
for x being object st x in dom IT1 holds
IT1 . x = IT2 . x

proof

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then consider m being Nat such that
A9: ( x = m + k & m in dom p ) by A5;
thus IT1 . x = p . m by A6, A9
.= IT2 . x by A8, A9 ; :: thesis: verum

end;

hence IT1 = IT2 by A5, A7; :: thesis: verum