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 S1[ 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 )
proof
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 ; :: thesis: verum
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)) } & S1[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: ( 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)) } & S1[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)) } & S1[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 ;
reconsider e = k as Element of NAT by ORDINAL1:def 12;
A12: e + 1 in Seg (N + 1) by ;
per cases ( ( m < i & k < i ) or ( m >= i & k < i ) or ( m < i & k >= i ) or ( m >= i & k >= i ) ) ;
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)) } & S1[x,y] )

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 ;
then A15: {k,m} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by ;
S1[{k,m},{k,m}] by ;
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)) } & S1[x,y] ) by ; :: thesis: verum
end;
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)) } & S1[x,y] )

A17: S1[{k,m},{k,(m + 1)}]
proof
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 ;
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 ; :: thesis: verum
end;
m + 1 > i by ;
then A19: not {k,(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by ;
m + 1 > k by ;
then {k,(m + 1)} in 2Set (Seg (n + 1)) by ;
then {k,(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by ;
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)) } & S1[x,y] ) by ; :: thesis: verum
end;
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)) } & S1[x,y] )

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)) } & S1[x,y] ) by ; :: thesis: verum
end;
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)) } & S1[x,y] )

A21: S1[{k,m},{(k + 1),(m + 1)}]
proof
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 ;
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 ; :: thesis: verum
end;
A24: k + 1 > i by ;
m + 1 > k + 1 by ;
then A25: {(k + 1),(m + 1)} in 2Set (Seg (n + 1)) by ;
m + 1 > i by ;
then not {(k + 1),(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by ;
then {(k + 1),(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } by ;
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)) } & S1[x,y] ) by ; :: thesis: verum
end;
end;
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
S1[x,f . x] from ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[{1,2},y] ) by ;
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: ( 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 ;
A33: ( k <> i & m <> i )
proof
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 ;
hence contradiction by A28, XBOOLE_0:def 5; :: thesis: verum
end;
A34: 1 <= m by ;
1 <= k by ;
then reconsider k1 = k - 1, m1 = m - 1 as Element of NAT by ;
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 ;
suppose A35: ( k < i & m < i ) ; :: thesis: x in rng f
A36: i <= n + 1 by ;
then k < n + 1 by ;
then A37: k <= n by NAT_1:13;
m < n + 1 by ;
then A38: m <= n by NAT_1:13;
1 <= m by ;
then A39: m in Seg n by A38;
A40: dom f = 2Set (Seg n) by FUNCT_2:def 1;
1 <= k by ;
then k in Seg n by A37;
then A41: {k9,m9} in 2Set (Seg n) by ;
then x = f . x by A26, A31, A32, A35;
hence x in rng f by ; :: thesis: verum
end;
suppose ( k > i & m < i ) ; :: thesis: x in rng f
hence x in rng f by ; :: thesis: verum
end;
suppose A42: ( k < i & m > i ) ; :: thesis: x in rng f
1 <= i by ;
then A43: 1 < m1 + 1 by ;
then A44: i <= m1 by ;
then A45: k < m1 by ;
i <= n + 1 by ;
then k < n + 1 by ;
then A46: k <= n by NAT_1:13;
A47: dom f = 2Set (Seg n) by FUNCT_2:def 1;
m1 + 1 <= n + 1 by ;
then m1 < n + 1 by NAT_1:13;
then A48: m1 <= n by NAT_1:13;
1 <= m1 by ;
then A49: m1 in Seg n by A48;
1 <= k by ;
then k in Seg n by A46;
then A50: {k9,m1} in 2Set (Seg n) by ;
then f . {k9,m1} = {k9,(m1 + 1)} by A26, A42, A44, A45;
hence x in rng f by ; :: thesis: verum
end;
suppose A51: ( k > i & m > i ) ; :: thesis: x in rng f
k1 + 1 <= n + 1 by ;
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 ;
then m1 < n + 1 by NAT_1:13;
then A54: m1 <= n by NAT_1:13;
A55: k1 < m1 by ;
A56: 1 <= i by ;
then A57: 1 < m1 + 1 by ;
A58: 1 < k1 + 1 by ;
then A59: i <= k1 by ;
1 <= k1 by ;
then A60: k1 in Seg n by A52;
1 <= m1 by ;
then m1 in Seg n by A54;
then A61: {k1,m1} in 2Set (Seg n) by ;
i <= m1 by ;
then f . {k1,m1} = {(k1 + 1),(m1 + 1)} by A26, A59, A55, A61;
hence x in rng f by ; :: thesis: verum
end;
end;
end;
A62: rng f c= SSX by RELAT_1:def 19;
then A63: SSX = rng f by ;
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 ;
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
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 ;
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 ;
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 ) ) ) ) ;
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;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
( k1 = k2 or k1 = m2 + 1 ) by ;
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose ( ( k1 >= i & m1 < i ) or ( k2 >= i & m2 < i ) ) ; :: thesis: x1 = x2
hence x1 = x2 by ; :: thesis: verum
end;
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 ;
( k1 + 1 = k2 + 1 or k1 + 1 = m2 + 1 ) by ;
hence x1 = x2 by A69, A70, A68, A83; :: thesis: verum
end;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
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 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 ; :: thesis: verum