let n, i be Nat; 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; ( 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 ) )
; ( (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
; a = b
A6:
now for x being Element of NAT st x >= i + 1 & x < n holds
a . x = b . xlet x be
Element of
NAT ;
( x >= i + 1 & x < n implies a . x = b . x )assume that A7:
x >= i + 1
and A8:
x < n
;
a . x = b . xset 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;
verum end;
hence
a = b
by PBOOLE:3; verum