let n, i be Nat; :: thesis: for a, b being ManySortedSet of n holds
( a = b iff ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & ((i + 1),n) -cut a = ((i + 1),n) -cut b ) )
let a, b be ManySortedSet of n; :: thesis: ( a = b iff ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & ((i + 1),n) -cut a = ((i + 1),n) -cut b ) )
set CUTA1 = (0,(i + 1)) -cut a;
set CUTA2 = ((i + 1),n) -cut a;
set CUTB1 = (0,(i + 1)) -cut b;
set CUTB2 = ((i + 1),n) -cut b;
thus ( a = b implies ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & ((i + 1),n) -cut a = ((i + 1),n) -cut b ) ) ; :: thesis: ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b & ((i + 1),n) -cut a = ((i + 1),n) -cut b implies a = b )
assume that
A1: (0,(i + 1)) -cut a = (0,(i + 1)) -cut b and
A2: ((i + 1),n) -cut a = ((i + 1),n) -cut b ; :: thesis: a = b

A3: now :: thesis: for k being Element of NAT st k in i + 1 holds
a . k = b . k

let k be Element of NAT ; :: thesis: ( k in i + 1 implies a . k = b . k )
assume A4: k in i + 1 ; :: thesis: a . k = b . k
(i + 1) -' 0 = ((i + 1) + 0) -' 0 ;
then A5: k in (i + 1) -' 0 by A4, NAT_D:34;
then ((0,(i + 1)) -cut b) . k = b . (0 + k) by Def1;
hence a . k = b . k by A1, A5, Def1; :: thesis: verum

end;

A6: now :: thesis: for x being Element of NAT st x >= i + 1 & x < n holds
a . x = b . x

let x be Element of NAT ; :: thesis: ( x >= i + 1 & x < n implies a . x = b . x )
assume that
A7: x >= i + 1 and
A8: x < n ; :: thesis: a . x = b . x
set k = x -' (i + 1);
x - (i + 1) >= (i + 1) - (i + 1) by A7, XREAL_1:9;
then A9: x -' (i + 1) = x - (i + 1) by XREAL_0:def 2;
n >= i + 1 by A7, A8, XXREAL_0:2;
then n - (i + 1) >= (i + 1) - (i + 1) by XREAL_1:9;
then A10: n -' (i + 1) = n - (i + 1) by XREAL_0:def 2;
x - (i + 1) < n - (i + 1) by A8, XREAL_1:14;
then A11: x -' (i + 1) in Segm (n -' (i + 1)) by A9, A10, NAT_1:44;
then (((i + 1),n) -cut b) . (x -' (i + 1)) = b . ((i + 1) + (x -' (i + 1))) by Def1;
hence a . x = b . x by A2, A9, A11, Def1; :: thesis: verum

end;

now :: thesis: for x9 being object st x9 in n holds
a . x9 = b . x9

let x9 be object ; :: thesis: ( x9 in n implies a . b₁ = b . b₁ )
assume A12: x9 in n ; :: thesis: a . b₁ = b . b₁
n = { k where k is Nat : k < n } by AXIOMS:4;
then A13: ex k being Nat st
( k = x9 & k < n ) by A12;
then reconsider x = x9 as Element of NAT by ORDINAL1:def 12;

per cases ( x in i + 1 or not x in Segm (i + 1) ) ;

suppose x in i + 1 ; :: thesis: a . b₁ = b . b₁

hence a . x9 = b . x9 by A3; :: thesis: verum

end;

suppose not x in Segm (i + 1) ; :: thesis: a . b₁ = b . b₁

then x >= i + 1 by NAT_1:44;
hence a . x9 = b . x9 by A6, A13; :: thesis: verum

end;

end;

end;

hence a = b by PBOOLE:3; :: thesis: verum