let n, i be Element of NAT ; :: thesis: for a, b being ManySortedSet of 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 ; :: 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 A1: ( 0 ,(i + 1) -cut a = 0 ,(i + 1) -cut b & (i + 1),n -cut a = (i + 1),n -cut b ) ; :: thesis: a = b

A2: now

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

end;

A5: now

let x be Element of NAT ; :: thesis: ( x >= i + 1 & x < n implies a . x = b . x )
assume A6: ( x >= i + 1 & x < n ) ; :: thesis: a . x = b . x
set k = x -' (i + 1);
x - (i + 1) >= (i + 1) - (i + 1) by A6, XREAL_1:11;
then A7: x -' (i + 1) = x - (i + 1) by XREAL_0:def 2;
n >= i + 1 by A6, XXREAL_0:2;
then n - (i + 1) >= (i + 1) - (i + 1) by XREAL_1:11;
then A8: n -' (i + 1) = n - (i + 1) by XREAL_0:def 2;
x - (i + 1) < n - (i + 1) by A6, XREAL_1:16;
then A9: x -' (i + 1) in n -' (i + 1) by A7, A8, NAT_1:45;
then ((i + 1),n -cut b) . (x -' (i + 1)) = b . ((i + 1) + (x -' (i + 1))) by Def1;
hence a . x = b . x by A1, A7, A9, Def1; :: thesis: verum

end;

now

let x' be set ; :: thesis: ( x' in n implies a . b₁ = b . b₁ )
assume A10: x' in n ; :: thesis: a . b₁ = b . b₁
n = { k where k is Element of NAT : k < n } by AXIOMS:30;
then consider k being Element of NAT such that
A11: ( k = x' & k < n ) by A10;
reconsider x = x' as Element of NAT by A11;

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

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

hence a . x' = b . x' by A2; :: thesis: verum

end;

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

then ( x >= i + 1 & x < n ) by A11, NAT_1:45;
hence a . x' = b . x' by A5; :: thesis: verum

end;

end;

end;

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