let IT1, IT2 be ManySortedSet of j -' i; :: thesis: ( ( for k being Element of NAT st k in j -' i holds
IT1 . k = b . (i + k) ) & ( for k being Element of NAT st k in j -' i holds
IT2 . k = b . (i + k) ) implies IT1 = IT2 )
assume that
A6: for k being Element of NAT st k in j -' i holds
IT1 . k = b . (i + k) and
A7: for k being Element of NAT st k in j -' i holds
IT2 . k = b . (i + k) ; :: thesis: IT1 = IT2
A8: j -' i = dom IT1 by PARTFUN1:def 2;
A9: j -' i = dom IT2 by PARTFUN1:def 2;

now :: thesis: for x being object st x in j -' i holds
IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in j -' i implies IT1 . x = IT2 . x )
assume A10: x in j -' i ; :: thesis: IT1 . x = IT2 . x
j -' i = { k where k is Nat : k < j -' i } by AXIOMS:4;
then ex k being Nat st
( x = k & k < j -' i ) by A10;
then reconsider x9 = x as Element of NAT by ORDINAL1:def 12;
IT1 . x = b . (i + x9) by A6, A10;
hence IT1 . x = IT2 . x by A7, A10; :: thesis: verum

end;

hence IT1 = IT2 by A8, A9, FUNCT_1:2; :: thesis: verum