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

( 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

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;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

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

a . x = b . x

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;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

now :: thesis: for x9 being object st x9 in n holds

a . x9 = b . x9

hence
a = b
by PBOOLE:3; :: thesis: veruma . x9 = b . x9

let x9 be object ; :: thesis: ( x9 in n implies a . b_{1} = b . b_{1} )

assume A12: x9 in n ; :: thesis: a . b_{1} = b . b_{1}

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;

end;assume A12: x9 in n ; :: thesis: a . 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;