let IT1, IT2 be Function; :: thesis: ( dom IT1 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
IT1 . (m + k) = p . m ) & dom IT2 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
IT2 . (m + k) = p . m ) implies IT1 = IT2 )
assume that
A27: dom IT1 = { (m + k) where m is Element of NAT : m in dom p } and
A28: for m being Element of NAT st m in dom p holds
IT1 . (m + k) = p . m and
A29: dom IT2 = { (m + k) where m is Element of NAT : m in dom p } and
A30: for m being Element of NAT st m in dom p holds
IT2 . (m + k) = p . m ; :: thesis: IT1 = IT2
for x being set st x in dom IT1 holds
IT1 . x = IT2 . x

proof

let x be set ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then consider m being Element of NAT such that
A31: x = m + k and
A32: m in dom p by A27;
thus IT1 . x = p . m by A28, A31, A32
.= IT2 . x by A30, A31, A32 ; :: thesis: verum

end;

hence IT1 = IT2 by A27, A29, FUNCT_1:9; :: thesis: verum