let n be Nat; :: thesis: for i, j being Nat st i in Seg (n + 1) & n >= 2 holds

ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st

( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )

let i, j be Nat; :: thesis: ( i in Seg (n + 1) & n >= 2 implies ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st

( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) ) )

assume that

A1: i in Seg (n + 1) and

A2: n >= 2 ; :: thesis: ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st

( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )

defpred S_{1}[ object , object ] means for k, m being Nat st {k,m} = $1 & k < m holds

( ( m < i & k < i implies $2 = {k,m} ) & ( m >= i & k < i implies $2 = {k,(m + 1)} ) & ( m >= i & k >= i implies $2 = {(k + 1),(m + 1)} ) );

set X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ;

set SS = 2Set (Seg n);

set n1 = n + 1;

set SS1 = 2Set (Seg (n + 1));

A3: for k, m being Nat holds

( not {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } or k = i or m = i )

ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )

A26: for x being object st x in 2Set (Seg n) holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A5);

ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[{1,2},y] )
by A2, A5, MATRIX11:3;

then reconsider SSX = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } as non empty set ;

reconsider f = f as Function of (2Set (Seg n)),SSX ;

A27: SSX c= rng f

then A63: SSX = rng f by A27, XBOOLE_0:def 10;

dom f = 2Set (Seg n) by FUNCT_2:def 1;

then reconsider f = f as Function of (2Set (Seg n)),(2Set (Seg (n + 1))) by A63, FUNCT_2:2;

take f ; :: thesis: ( rng f = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & f is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) ) )

for x1, x2 being object st x1 in 2Set (Seg n) & x2 in 2Set (Seg n) & f . x1 = f . x2 holds

x1 = x2

( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) ) ) by A26, A27, A62, FUNCT_2:19, XBOOLE_0:def 10; :: thesis: verum

ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st

( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )

let i, j be Nat; :: thesis: ( i in Seg (n + 1) & n >= 2 implies ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st

( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) ) )

assume that

A1: i in Seg (n + 1) and

A2: n >= 2 ; :: thesis: ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st

( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )

defpred S

( ( m < i & k < i implies $2 = {k,m} ) & ( m >= i & k < i implies $2 = {k,(m + 1)} ) & ( m >= i & k >= i implies $2 = {(k + 1),(m + 1)} ) );

set X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ;

set SS = 2Set (Seg n);

set n1 = n + 1;

set SS1 = 2Set (Seg (n + 1));

A3: for k, m being Nat holds

( not {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } or k = i or m = i )

proof

A5:
for x being object st x in 2Set (Seg n) holds
let k, m be Nat; :: thesis: ( not {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } or k = i or m = i )

assume {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ; :: thesis: ( k = i or m = i )

then consider m1 being Nat such that

A4: {k,m} = {m1,i} and

{m1,i} in 2Set (Seg (n + 1)) ;

i in {i,m1} by TARSKI:def 2;

hence ( k = i or m = i ) by A4, TARSKI:def 2; :: thesis: verum

end;assume {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ; :: thesis: ( k = i or m = i )

then consider m1 being Nat such that

A4: {k,m} = {m1,i} and

{m1,i} in 2Set (Seg (n + 1)) ;

i in {i,m1} by TARSKI:def 2;

hence ( k = i or m = i ) by A4, TARSKI:def 2; :: thesis: verum

ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

proof

consider f being Function of (2Set (Seg n)),((2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ) such that
n <= n + 1
by NAT_1:11;

then A6: Seg n c= Seg (n + 1) by FINSEQ_1:5;

reconsider N = n as Element of NAT by ORDINAL1:def 12;

let x be object ; :: thesis: ( x in 2Set (Seg n) implies ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] ) )

assume x in 2Set (Seg n) ; :: thesis: ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )

then consider k, m being Nat such that

A7: k in Seg n and

A8: m in Seg n and

A9: k < m and

A10: x = {k,m} by MATRIX11:1;

A11: m + 1 in Seg (N + 1) by A8, FINSEQ_1:60;

reconsider e = k as Element of NAT by ORDINAL1:def 12;

A12: e + 1 in Seg (N + 1) by A7, FINSEQ_1:60;

end;then A6: Seg n c= Seg (n + 1) by FINSEQ_1:5;

reconsider N = n as Element of NAT by ORDINAL1:def 12;

let x be object ; :: thesis: ( x in 2Set (Seg n) implies ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

assume x in 2Set (Seg n) ; :: thesis: ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

then consider k, m being Nat such that

A7: k in Seg n and

A8: m in Seg n and

A9: k < m and

A10: x = {k,m} by MATRIX11:1;

A11: m + 1 in Seg (N + 1) by A8, FINSEQ_1:60;

reconsider e = k as Element of NAT by ORDINAL1:def 12;

A12: e + 1 in Seg (N + 1) by A7, FINSEQ_1:60;

per cases
( ( m < i & k < i ) or ( m >= i & k < i ) or ( m < i & k >= i ) or ( m >= i & k >= i ) )
;

end;

suppose A13:
( m < i & k < i )
; :: thesis: ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

then A14:
not {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A3;

{k,m} in 2Set (Seg (n + 1)) by A7, A8, A9, A6, MATRIX11:1;

then A15: {k,m} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A14, XBOOLE_0:def 5;

S_{1}[{k,m},{k,m}]
by A13, ZFMISC_1:6;

hence ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )
by A10, A15; :: thesis: verum

end;{k,m} in 2Set (Seg (n + 1)) by A7, A8, A9, A6, MATRIX11:1;

then A15: {k,m} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A14, XBOOLE_0:def 5;

S

hence ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

suppose A16:
( m >= i & k < i )
; :: thesis: ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

A17:
S_{1}[{k,m},{k,(m + 1)}]

then A19: not {k,(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A3, A16;

m + 1 > k by A9, NAT_1:13;

then {k,(m + 1)} in 2Set (Seg (n + 1)) by A7, A6, A11, MATRIX11:1;

then {k,(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A19, XBOOLE_0:def 5;

hence ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )
by A10, A17; :: thesis: verum

end;proof

m + 1 > i
by A16, NAT_1:13;
let k9, m9 be Nat; :: thesis: ( {k9,m9} = {k,m} & k9 < m9 implies ( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) )

assume that

A18: {k9,m9} = {k,m} and

k9 < m9 ; :: thesis: ( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) )

( k9 = k or k9 = m ) by A18, ZFMISC_1:6;

hence ( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) by A16, A18, ZFMISC_1:6; :: thesis: verum

end;assume that

A18: {k9,m9} = {k,m} and

k9 < m9 ; :: thesis: ( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) )

( k9 = k or k9 = m ) by A18, ZFMISC_1:6;

hence ( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) by A16, A18, ZFMISC_1:6; :: thesis: verum

then A19: not {k,(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A3, A16;

m + 1 > k by A9, NAT_1:13;

then {k,(m + 1)} in 2Set (Seg (n + 1)) by A7, A6, A11, MATRIX11:1;

then {k,(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A19, XBOOLE_0:def 5;

hence ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

suppose
( m < i & k >= i )
; :: thesis: ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

hence
ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )
by A9, XXREAL_0:2; :: thesis: verum

end;( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

suppose A20:
( m >= i & k >= i )
; :: thesis: ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

A21:
S_{1}[{k,m},{(k + 1),(m + 1)}]

m + 1 > k + 1 by A9, XREAL_1:8;

then A25: {(k + 1),(m + 1)} in 2Set (Seg (n + 1)) by A11, A12, MATRIX11:1;

m + 1 > i by A20, NAT_1:13;

then not {(k + 1),(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A3, A24;

then {(k + 1),(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A25, XBOOLE_0:def 5;

hence ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S_{1}[x,y] )
by A10, A21; :: thesis: verum

end;proof

A24:
k + 1 > i
by A20, NAT_1:13;
let k9, m9 be Nat; :: thesis: ( {k9,m9} = {k,m} & k9 < m9 implies ( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) )

assume that

A22: {k9,m9} = {k,m} and

A23: k9 < m9 ; :: thesis: ( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) )

( k9 = k or k9 = m ) by A22, ZFMISC_1:6;

hence ( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) by A20, A22, A23, ZFMISC_1:6; :: thesis: verum

end;assume that

A22: {k9,m9} = {k,m} and

A23: k9 < m9 ; :: thesis: ( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) )

( k9 = k or k9 = m ) by A22, ZFMISC_1:6;

hence ( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) by A20, A22, A23, ZFMISC_1:6; :: thesis: verum

m + 1 > k + 1 by A9, XREAL_1:8;

then A25: {(k + 1),(m + 1)} in 2Set (Seg (n + 1)) by A11, A12, MATRIX11:1;

m + 1 > i by A20, NAT_1:13;

then not {(k + 1),(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A3, A24;

then {(k + 1),(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A25, XBOOLE_0:def 5;

hence ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

A26: for x being object st x in 2Set (Seg n) holds

S

ex y being object st

( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S

then reconsider SSX = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } as non empty set ;

reconsider f = f as Function of (2Set (Seg n)),SSX ;

A27: SSX c= rng f

proof

A62:
rng f c= SSX
by RELAT_1:def 19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SSX or x in rng f )

assume A28: x in SSX ; :: thesis: x in rng f

consider k, m being Nat such that

A29: k in Seg (n + 1) and

A30: m in Seg (n + 1) and

A31: k < m and

A32: x = {k,m} by A28, MATRIX11:1;

A33: ( k <> i & m <> i )

1 <= k by A29, FINSEQ_1:1;

then reconsider k1 = k - 1, m1 = m - 1 as Element of NAT by A34, NAT_1:21;

reconsider m9 = m, k9 = k as Element of NAT by ORDINAL1:def 12;

end;assume A28: x in SSX ; :: thesis: x in rng f

consider k, m being Nat such that

A29: k in Seg (n + 1) and

A30: m in Seg (n + 1) and

A31: k < m and

A32: x = {k,m} by A28, MATRIX11:1;

A33: ( k <> i & m <> i )

proof

A34:
1 <= m
by A30, FINSEQ_1:1;
assume
( k = i or m = i )
; :: thesis: contradiction

then x in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A28, A32;

hence contradiction by A28, XBOOLE_0:def 5; :: thesis: verum

end;then x in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by A28, A32;

hence contradiction by A28, XBOOLE_0:def 5; :: thesis: verum

1 <= k by A29, FINSEQ_1:1;

then reconsider k1 = k - 1, m1 = m - 1 as Element of NAT by A34, NAT_1:21;

reconsider m9 = m, k9 = k as Element of NAT by ORDINAL1:def 12;

per cases
( ( k < i & m < i ) or ( k > i & m < i ) or ( k < i & m > i ) or ( k > i & m > i ) )
by A33, XXREAL_0:1;

end;

suppose A35:
( k < i & m < i )
; :: thesis: x in rng f

A36:
i <= n + 1
by A1, FINSEQ_1:1;

then k < n + 1 by A35, XXREAL_0:2;

then A37: k <= n by NAT_1:13;

m < n + 1 by A35, A36, XXREAL_0:2;

then A38: m <= n by NAT_1:13;

1 <= m by A30, FINSEQ_1:1;

then A39: m in Seg n by A38;

A40: dom f = 2Set (Seg n) by FUNCT_2:def 1;

1 <= k by A29, FINSEQ_1:1;

then k in Seg n by A37;

then A41: {k9,m9} in 2Set (Seg n) by A31, A39, MATRIX11:1;

then x = f . x by A26, A31, A32, A35;

hence x in rng f by A32, A41, A40, FUNCT_1:def 3; :: thesis: verum

end;then k < n + 1 by A35, XXREAL_0:2;

then A37: k <= n by NAT_1:13;

m < n + 1 by A35, A36, XXREAL_0:2;

then A38: m <= n by NAT_1:13;

1 <= m by A30, FINSEQ_1:1;

then A39: m in Seg n by A38;

A40: dom f = 2Set (Seg n) by FUNCT_2:def 1;

1 <= k by A29, FINSEQ_1:1;

then k in Seg n by A37;

then A41: {k9,m9} in 2Set (Seg n) by A31, A39, MATRIX11:1;

then x = f . x by A26, A31, A32, A35;

hence x in rng f by A32, A41, A40, FUNCT_1:def 3; :: thesis: verum

suppose A42:
( k < i & m > i )
; :: thesis: x in rng f

1 <= i
by A1, FINSEQ_1:1;

then A43: 1 < m1 + 1 by A42, XXREAL_0:2;

then A44: i <= m1 by A42, NAT_1:13;

then A45: k < m1 by A42, XXREAL_0:2;

i <= n + 1 by A1, FINSEQ_1:1;

then k < n + 1 by A42, XXREAL_0:2;

then A46: k <= n by NAT_1:13;

A47: dom f = 2Set (Seg n) by FUNCT_2:def 1;

m1 + 1 <= n + 1 by A30, FINSEQ_1:1;

then m1 < n + 1 by NAT_1:13;

then A48: m1 <= n by NAT_1:13;

1 <= m1 by A43, NAT_1:13;

then A49: m1 in Seg n by A48;

1 <= k by A29, FINSEQ_1:1;

then k in Seg n by A46;

then A50: {k9,m1} in 2Set (Seg n) by A49, A45, MATRIX11:1;

then f . {k9,m1} = {k9,(m1 + 1)} by A26, A42, A44, A45;

hence x in rng f by A32, A50, A47, FUNCT_1:def 3; :: thesis: verum

end;then A43: 1 < m1 + 1 by A42, XXREAL_0:2;

then A44: i <= m1 by A42, NAT_1:13;

then A45: k < m1 by A42, XXREAL_0:2;

i <= n + 1 by A1, FINSEQ_1:1;

then k < n + 1 by A42, XXREAL_0:2;

then A46: k <= n by NAT_1:13;

A47: dom f = 2Set (Seg n) by FUNCT_2:def 1;

m1 + 1 <= n + 1 by A30, FINSEQ_1:1;

then m1 < n + 1 by NAT_1:13;

then A48: m1 <= n by NAT_1:13;

1 <= m1 by A43, NAT_1:13;

then A49: m1 in Seg n by A48;

1 <= k by A29, FINSEQ_1:1;

then k in Seg n by A46;

then A50: {k9,m1} in 2Set (Seg n) by A49, A45, MATRIX11:1;

then f . {k9,m1} = {k9,(m1 + 1)} by A26, A42, A44, A45;

hence x in rng f by A32, A50, A47, FUNCT_1:def 3; :: thesis: verum

suppose A51:
( k > i & m > i )
; :: thesis: x in rng f

k1 + 1 <= n + 1
by A29, FINSEQ_1:1;

then k1 < n + 1 by NAT_1:13;

then A52: k1 <= n by NAT_1:13;

A53: dom f = 2Set (Seg n) by FUNCT_2:def 1;

m1 + 1 <= n + 1 by A30, FINSEQ_1:1;

then m1 < n + 1 by NAT_1:13;

then A54: m1 <= n by NAT_1:13;

A55: k1 < m1 by A31, XREAL_1:9;

A56: 1 <= i by A1, FINSEQ_1:1;

then A57: 1 < m1 + 1 by A51, XXREAL_0:2;

A58: 1 < k1 + 1 by A51, A56, XXREAL_0:2;

then A59: i <= k1 by A51, NAT_1:13;

1 <= k1 by A58, NAT_1:13;

then A60: k1 in Seg n by A52;

1 <= m1 by A57, NAT_1:13;

then m1 in Seg n by A54;

then A61: {k1,m1} in 2Set (Seg n) by A60, A55, MATRIX11:1;

i <= m1 by A51, A57, NAT_1:13;

then f . {k1,m1} = {(k1 + 1),(m1 + 1)} by A26, A59, A55, A61;

hence x in rng f by A32, A61, A53, FUNCT_1:def 3; :: thesis: verum

end;then k1 < n + 1 by NAT_1:13;

then A52: k1 <= n by NAT_1:13;

A53: dom f = 2Set (Seg n) by FUNCT_2:def 1;

m1 + 1 <= n + 1 by A30, FINSEQ_1:1;

then m1 < n + 1 by NAT_1:13;

then A54: m1 <= n by NAT_1:13;

A55: k1 < m1 by A31, XREAL_1:9;

A56: 1 <= i by A1, FINSEQ_1:1;

then A57: 1 < m1 + 1 by A51, XXREAL_0:2;

A58: 1 < k1 + 1 by A51, A56, XXREAL_0:2;

then A59: i <= k1 by A51, NAT_1:13;

1 <= k1 by A58, NAT_1:13;

then A60: k1 in Seg n by A52;

1 <= m1 by A57, NAT_1:13;

then m1 in Seg n by A54;

then A61: {k1,m1} in 2Set (Seg n) by A60, A55, MATRIX11:1;

i <= m1 by A51, A57, NAT_1:13;

then f . {k1,m1} = {(k1 + 1),(m1 + 1)} by A26, A59, A55, A61;

hence x in rng f by A32, A61, A53, FUNCT_1:def 3; :: thesis: verum

then A63: SSX = rng f by A27, XBOOLE_0:def 10;

dom f = 2Set (Seg n) by FUNCT_2:def 1;

then reconsider f = f as Function of (2Set (Seg n)),(2Set (Seg (n + 1))) by A63, FUNCT_2:2;

take f ; :: thesis: ( rng f = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & f is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds

( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) ) )

for x1, x2 being object st x1 in 2Set (Seg n) & x2 in 2Set (Seg n) & f . x1 = f . x2 holds

x1 = x2

proof

hence
( rng f = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & f is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
let x1, x2 be object ; :: thesis: ( x1 in 2Set (Seg n) & x2 in 2Set (Seg n) & f . x1 = f . x2 implies x1 = x2 )

assume that

A64: x1 in 2Set (Seg n) and

A65: x2 in 2Set (Seg n) and

A66: f . x1 = f . x2 ; :: thesis: x1 = x2

consider k2, m2 being Nat such that

k2 in Seg n and

m2 in Seg n and

A67: k2 < m2 and

A68: x2 = {k2,m2} by A65, MATRIX11:1;

consider k1, m1 being Nat such that

k1 in Seg n and

m1 in Seg n and

A69: k1 < m1 and

A70: x1 = {k1,m1} by A64, MATRIX11:1;

reconsider m1 = m1, m2 = m2, k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def 12;

end;assume that

A64: x1 in 2Set (Seg n) and

A65: x2 in 2Set (Seg n) and

A66: f . x1 = f . x2 ; :: thesis: x1 = x2

consider k2, m2 being Nat such that

k2 in Seg n and

m2 in Seg n and

A67: k2 < m2 and

A68: x2 = {k2,m2} by A65, MATRIX11:1;

consider k1, m1 being Nat such that

k1 in Seg n and

m1 in Seg n and

A69: k1 < m1 and

A70: x1 = {k1,m1} by A64, MATRIX11:1;

reconsider m1 = m1, m2 = m2, k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def 12;

per cases
( ( k1 < i & m1 < i & k2 < i & m2 < i ) or ( k1 < i & m1 < i & ( k2 < i or k2 >= i ) & m2 >= i ) or ( k1 < i & m1 >= i & k2 < i & m2 >= i ) or ( k1 < i & m1 >= i & ( ( k2 >= i & m2 >= i ) or ( k2 < i & m2 < i ) ) ) or ( k1 >= i & m1 < i ) or ( k2 >= i & m2 < i ) or ( k1 >= i & m1 >= i & k2 >= i & m2 >= i ) or ( k1 >= i & m1 >= i & ( ( k2 < i & m2 < i ) or ( k2 < i & m2 >= i ) ) ) )
;

end;

suppose A71:
( k1 < i & m1 < i & k2 < i & m2 < i )
; :: thesis: x1 = x2

then
f . x1 = x1
by A26, A64, A69, A70;

hence x1 = x2 by A26, A65, A66, A67, A68, A71; :: thesis: verum

end;hence x1 = x2 by A26, A65, A66, A67, A68, A71; :: thesis: verum

suppose A72:
( k1 < i & m1 < i & ( k2 < i or k2 >= i ) & m2 >= i )
; :: thesis: x1 = x2

then A73:
( f . x2 = {k2,(m2 + 1)} or f . x2 = {(k2 + 1),(m2 + 1)} )
by A26, A65, A67, A68;

f . x1 = {k1,m1} by A26, A64, A69, A70, A72;

then ( ( ( k1 = k2 or k1 = m2 + 1 ) & ( m1 = k2 or m1 = m2 + 1 ) ) or ( ( k1 = k2 + 1 or k1 = m2 + 1 ) & ( m1 = k2 + 1 or m1 = m2 + 1 ) ) ) by A66, A73, ZFMISC_1:6;

hence x1 = x2 by A69, A72, NAT_1:13; :: thesis: verum

end;f . x1 = {k1,m1} by A26, A64, A69, A70, A72;

then ( ( ( k1 = k2 or k1 = m2 + 1 ) & ( m1 = k2 or m1 = m2 + 1 ) ) or ( ( k1 = k2 + 1 or k1 = m2 + 1 ) & ( m1 = k2 + 1 or m1 = m2 + 1 ) ) ) by A66, A73, ZFMISC_1:6;

hence x1 = x2 by A69, A72, NAT_1:13; :: thesis: verum

suppose A74:
( k1 < i & m1 >= i & k2 < i & m2 >= i )
; :: thesis: x1 = x2

then A75:
f . x2 = {k2,(m2 + 1)}
by A26, A65, A67, A68;

A76: f . x1 = {k1,(m1 + 1)} by A26, A64, A69, A70, A74;

then A77: ( m1 + 1 = k2 or m1 + 1 = m2 + 1 ) by A66, A75, ZFMISC_1:6;

( k1 = k2 or k1 = m2 + 1 ) by A66, A76, A75, ZFMISC_1:6;

hence x1 = x2 by A70, A68, A74, A77, NAT_1:13; :: thesis: verum

end;A76: f . x1 = {k1,(m1 + 1)} by A26, A64, A69, A70, A74;

then A77: ( m1 + 1 = k2 or m1 + 1 = m2 + 1 ) by A66, A75, ZFMISC_1:6;

( k1 = k2 or k1 = m2 + 1 ) by A66, A76, A75, ZFMISC_1:6;

hence x1 = x2 by A70, A68, A74, A77, NAT_1:13; :: thesis: verum

suppose A78:
( k1 < i & m1 >= i & ( ( k2 >= i & m2 >= i ) or ( k2 < i & m2 < i ) ) )
; :: thesis: x1 = x2

then A79:
( f . x2 = {(k2 + 1),(m2 + 1)} or f . x2 = {k2,m2} )
by A26, A65, A67, A68;

f . x1 = {k1,(m1 + 1)} by A26, A64, A69, A70, A78;

then ( ( ( k1 = k2 + 1 or k1 = m2 + 1 ) & ( m1 + 1 = k2 + 1 or m1 + 1 = m2 + 1 ) ) or ( ( k1 = k2 or k1 = m2 ) & ( m1 + 1 = k2 or m1 + 1 = m2 ) ) ) by A66, A79, ZFMISC_1:6;

hence x1 = x2 by A78, NAT_1:13; :: thesis: verum

end;f . x1 = {k1,(m1 + 1)} by A26, A64, A69, A70, A78;

then ( ( ( k1 = k2 + 1 or k1 = m2 + 1 ) & ( m1 + 1 = k2 + 1 or m1 + 1 = m2 + 1 ) ) or ( ( k1 = k2 or k1 = m2 ) & ( m1 + 1 = k2 or m1 + 1 = m2 ) ) ) by A66, A79, ZFMISC_1:6;

hence x1 = x2 by A78, NAT_1:13; :: thesis: verum

suppose A80:
( k1 >= i & m1 >= i & k2 >= i & m2 >= i )
; :: thesis: x1 = x2

then A81:
f . x2 = {(k2 + 1),(m2 + 1)}
by A26, A65, A67, A68;

A82: f . x1 = {(k1 + 1),(m1 + 1)} by A26, A64, A69, A70, A80;

then A83: ( m1 + 1 = k2 + 1 or m1 + 1 = m2 + 1 ) by A66, A81, ZFMISC_1:6;

( k1 + 1 = k2 + 1 or k1 + 1 = m2 + 1 ) by A66, A82, A81, ZFMISC_1:6;

hence x1 = x2 by A69, A70, A68, A83; :: thesis: verum

end;A82: f . x1 = {(k1 + 1),(m1 + 1)} by A26, A64, A69, A70, A80;

then A83: ( m1 + 1 = k2 + 1 or m1 + 1 = m2 + 1 ) by A66, A81, ZFMISC_1:6;

( k1 + 1 = k2 + 1 or k1 + 1 = m2 + 1 ) by A66, A82, A81, ZFMISC_1:6;

hence x1 = x2 by A69, A70, A68, A83; :: thesis: verum

suppose A84:
( k1 >= i & m1 >= i & ( ( k2 < i & m2 < i ) or ( k2 < i & m2 >= i ) ) )
; :: thesis: x1 = x2

then A85:
( f . x2 = {k2,m2} or f . x2 = {k2,(m2 + 1)} )
by A26, A65, A67, A68;

f . x1 = {(k1 + 1),(m1 + 1)} by A26, A64, A69, A70, A84;

then ( ( ( k1 + 1 = k2 or k1 + 1 = m2 ) & ( m1 + 1 = k2 or m1 + 1 = m2 ) ) or ( ( k1 + 1 = k2 or k1 + 1 = m2 + 1 ) & ( m1 + 1 = k2 or m1 + 1 = m2 + 1 ) ) ) by A66, A85, ZFMISC_1:6;

hence x1 = x2 by A69, A84, NAT_1:13; :: thesis: verum

end;f . x1 = {(k1 + 1),(m1 + 1)} by A26, A64, A69, A70, A84;

then ( ( ( k1 + 1 = k2 or k1 + 1 = m2 ) & ( m1 + 1 = k2 or m1 + 1 = m2 ) ) or ( ( k1 + 1 = k2 or k1 + 1 = m2 + 1 ) & ( m1 + 1 = k2 or m1 + 1 = m2 + 1 ) ) ) by A66, A85, ZFMISC_1:6;

hence x1 = x2 by A69, A84, NAT_1:13; :: thesis: verum

( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) ) ) by A26, A27, A62, FUNCT_2:19, XBOOLE_0:def 10; :: thesis: verum