let n be Nat; :: thesis:
let i, j be Nat; :: thesis:
assume that
A1: i in Seg (n + 1) and
A2: n >= 2 ; :: thesis:
defpred S₁[ object , object ] means for k, m being Nat st {k,m} = $1 & k < m holds
( ( m = i & k = 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 )

let k, m be Nat; :: thesis:
assume {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ; :: thesis:
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:

end;

A5: for x being object st x in 2Set (Seg n) holds
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₁[x,y] )

proof

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:
assume x in 2Set (Seg n) ; :: thesis:
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 ;

suppose A13: ( m < i & k < i ) ; :: thesis:

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₁[{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₁[x,y] ) by A10, A15; :: thesis:

end;

suppose A16: ( m >= i & k < i ) ; :: thesis:

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

proof

let k9, m9 be Nat; :: thesis:
assume that
A18: {k9,m9} = {k,m} and
k9 < m9 ; :: thesis:
( k9 = k or k9 = m ) by A18, ZFMISC_1:6;
hence ( ( m9 = i & k9 = i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) by A16, A18, ZFMISC_1:6; :: thesis:

end;

m + 1 > i by A16, NAT_1:13;
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₁[x,y] ) by A10, A17; :: thesis:

end;

suppose ( m = i ) ; :: thesis:

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₁[x,y] ) by A9, XXREAL_0:2; :: thesis:

end;

suppose A20: ( m >= i & k >= i ) ; :: thesis:

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

proof

let k9, m9 be Nat; :: thesis:
assume that
A22: {k9,m9} = {k,m} and
A23: k9 < m9 ; :: thesis:
( k9 = k or k9 = m ) by A22, ZFMISC_1:6;
hence ( ( m9 = i & k9 = i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) by A20, A22, A23, ZFMISC_1:6; :: thesis:

end;

A24: k + 1 > i by A20, NAT_1:13;
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₁[x,y] ) by A10, A21; :: thesis:

end;

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
A26: for x being object st x in 2Set (Seg n) holds
S₁[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,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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A28: x in SSX ; :: thesis:
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

assume ( k = i or m = i ) ; :: thesis:
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:

end;

A34: 1 <= m by A30, FINSEQ_1:1;
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 by A33, XXREAL_0:1;

suppose A35: ( k < i & m < i ) ; :: thesis:

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:

end;

suppose ( k > i & m < i ) ; :: thesis:

hence x in rng f by A31, XXREAL_0:2; :: thesis:

end;

suppose A42: ( k i ) ; :: thesis:

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:

end;

suppose A51: ( k > i & m > i ) ; :: thesis:

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:

end;

A62: rng f c= SSX by RELAT_1:def 19;
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:
for x1, x2 being object st x1 in 2Set (Seg n) & x2 in 2Set (Seg n) & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume that
A64: x1 in 2Set (Seg n) and
A65: x2 in 2Set (Seg n) and
A66: f . x1 = f . x2 ; :: thesis:
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 ;

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

then f . x1 = x1 by A26, A64, A69, A70;
hence x1 = x2 by A26, A65, A66, A67, A68, A71; :: thesis:

end;

suppose A72: ( k1 = i ) & m2 >= i ) ; :: thesis:

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:

end;

suppose A74: ( k1 = i & k2 = i ) ; :: thesis:

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:

end;

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

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:

end;

suppose ( ( k1 >= i & m1 = i & m2 < i ) ) ; :: thesis:

hence x1 = x2 by A69, A67, XXREAL_0:2; :: thesis:

end;

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

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:

end;

suppose A84: ( k1 >= i & m1 >= i & ( ( k2 = i ) ) ) ; :: thesis:

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:

end;

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