let IT1, IT2 be FinPartState of S; :: thesis: ( dom IT1 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
IT1 . (il. S,(m + k)) = p . (il. S,m) ) & dom IT2 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } & ( for m being Element of NAT st il. S,m in dom p holds
IT2 . (il. S,(m + k)) = p . (il. S,m) ) implies IT1 = IT2 )
assume that
A20: dom IT1 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } and
A21: for m being Element of NAT st il. S,m in dom p holds
IT1 . (il. S,(m + k)) = p . (il. S,m) and
A22: dom IT2 = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } and
A23: for m being Element of NAT st il. S,m in dom p holds
IT2 . (il. S,(m + k)) = p . (il. S,m) ; :: thesis: IT1 = IT2
for x being set st x in { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } holds
IT1 . x = IT2 . x

proof

let x be set ; :: thesis: ( x in { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } implies IT1 . x = IT2 . x )
assume x in { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom p } ; :: thesis: IT1 . x = IT2 . x
then consider m being Element of NAT such that
A24: x = il. S,(m + k) and
A25: il. S,m in dom p ;
thus IT1 . x = p . (il. S,m) by A21, A24, A25
.= IT2 . x by A23, A24, A25 ; :: thesis: verum

end;

hence IT1 = IT2 by A20, A22, FUNCT_1:9; :: thesis: verum