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