let y be set ; :: thesis:
let i, n be Nat; :: thesis:
set x1 = { k where k is Element of NAT : ( k in y & k i ) } ;
set x = { k where k is Element of NAT : ( k in y & k i ) } ;
set f1 = id { k where k is Element of NAT : ( k in y & k < i ) } ;
assume A1: y c= Seg (n + 1) ; :: thesis:
then A2: y = rng (Sgm y) by FINSEQ_1:def 13;
assume A3: i in Seg (n + 1) ; :: thesis:
then A4: 1 <= i by FINSEQ_1:1;
A5: i <= n + 1 by A3, FINSEQ_1:1;

let z be object ; :: thesis:
assume A7: z in { k where k is Element of NAT : ( k in y & k i ) } ; :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose z in { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis:

then A8: ex k being Element of NAT st
( k = z & k in y & k < i ) ;
then reconsider z9 = z as Element of NAT ;
z9 < n + 1 by A5, A8, XXREAL_0:2;
then A9: z9 <= n by NAT_1:13;
1 <= z9 by A1, A8, FINSEQ_1:1;
hence z in Seg n by A9; :: thesis:

end;

suppose z in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis:

then consider k being Element of NAT such that
A10: k - 1 = z and
A11: k in y and
A12: k > i ;
reconsider z9 = z as Integer by A10;
1 < k by A4, A12, XXREAL_0:2;
then 1 + 1 < k + 1 by XREAL_1:6;
then 2 <= k by NAT_1:13;
then A13: 2 - 1 <= k - 1 by XREAL_1:9;
then reconsider z9 = z9 as Element of NAT by A10, INT_1:3;
k <= n + 1 by A1, A11, FINSEQ_1:1;
then k - 1 <= (n + 1) - 1 by XREAL_1:9;
then z9 <= n by A10;
hence z in Seg n by A10, A13; :: thesis:

end;

then A14: { k where k is Element of NAT : ( k in y & k i ) } c= Seg n ;
then reconsider x9 = { k where k is Element of NAT : ( k in y & k i ) } , y9 = y as finite set by A1;
set f2 = { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } ;

now :: thesis:

let x be object ; :: thesis:
assume x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } ; :: thesis:
then consider k being Element of NAT such that
A15: [(k - 1),k] = x and
k in y9 and
k > i ;
reconsider y = k - 1, z = k as object ;
take y = y; :: thesis:
take z = z; :: thesis:
thus x = [y,z] by A15; :: thesis:

end;

then reconsider f2 = { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } as Relation by RELAT_1:def 1;
set f = (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2;

A16: now :: thesis:

let x be object ; :: thesis:
assume x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis:
then consider k being Element of NAT such that
A17: ( k - 1 = x & k in y9 & k > i ) ;
reconsider y = k as set ;
[x,y] in f2 by A17;
hence x in dom f2 by XTUPLE_0:def 12; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume x in dom f2 ; :: thesis:
then consider y being object such that
A18: [x,y] in f2 by XTUPLE_0:def 12;
consider k being Element of NAT such that
A19: [(k - 1),k] = [x,y] and
A20: ( k in y9 & k > i ) by A18;
k - 1 = x by A19, XTUPLE_0:1;
hence x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } by A20; :: thesis:

end;

then A21: dom f2 = { (k - 1) where k is Element of NAT : ( k in y & k > i ) } by A16, TARSKI:2;

A22: now :: thesis:

let x, y1, y2 be object ; :: thesis:
assume A23: [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis:
assume A24: [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis:
A25: ( y1 is set & y2 is set ) by TARSKI:1;

per cases in id { k where k is Element of NAT : ( k in y & k < i ) } or [x,y1] in f2 ) by A23, XBOOLE_0:def 3;

suppose A26: [x,y1] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis:

then A27: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by XTUPLE_0:def 12;
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x = x by FUNCT_1:17;
then A28: y1 = x by A26, A27, FUNCT_1:def 2, A25;

per cases in id { k where k is Element of NAT : ( k in y & k < i ) } or [x,y2] in f2 ) by A24, XBOOLE_0:def 3;

suppose A29: [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis:

then A30: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by XTUPLE_0:def 12;
then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x = x by FUNCT_1:17;
hence y1 = y2 by A28, A29, A30, FUNCT_1:def 2, A25; :: thesis:

end;

suppose A31: [x,y2] in f2 ; :: thesis:

x in { k where k is Element of NAT : ( k in y & k i ) } by A21, A31, XTUPLE_0:def 12;
then ex k being Element of NAT st
( k - 1 = x & k in y & k > i ) ;
then k9 + 1 > i by A32;
hence y1 = y2 by A33, NAT_1:13; :: thesis:

end;

suppose [x,y1] in f2 ; :: thesis:

then consider k being Element of NAT such that
A34: [(k - 1),k] = [x,y1] and
k in y9 and
A35: k > i ;
A36: k - 1 = x by A34, XTUPLE_0:1;

per cases in id { k where k is Element of NAT : ( k in y & k < i ) } or [x,y2] in f2 ) by A24, XBOOLE_0:def 3;

suppose [x,y2] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis:

then x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by XTUPLE_0:def 12;
then x in { k where k is Element of NAT : ( k in y & k i by A35;
hence y1 = y2 by A38, NAT_1:13; :: thesis:

end;

suppose [x,y2] in f2 ; :: thesis:

then consider k9 being Element of NAT such that
A39: [(k9 - 1),k9] = [x,y2] and
k9 in y9 and
k9 > i ;
k9 - 1 = x by A39, XTUPLE_0:1;
hence y1 = y2 by A34, A36, A39, XTUPLE_0:1; :: thesis:

end;

A40: now :: thesis:

let x, y1, y2 be object ; :: thesis:
assume [x,y1] in f2 ; :: thesis:
then consider k being Element of NAT such that
A41: [(k - 1),k] = [x,y1] and
k in y9 and
k > i ;
A42: k - 1 = x by A41, XTUPLE_0:1;
assume [x,y2] in f2 ; :: thesis:
then consider k9 being Element of NAT such that
A43: [(k9 - 1),k9] = [x,y2] and
k9 in y9 and
k9 > i ;
k9 - 1 = x by A43, XTUPLE_0:1;
hence y1 = y2 by A41, A43, A42, XTUPLE_0:1; :: thesis:

end;

reconsider f = (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 as Function by A22, FUNCT_1:def 1;

A44: now :: thesis:

let x be object ; :: thesis:
A45: id { k where k is Element of NAT : ( k in y & k < i ) } c= f by XBOOLE_1:7;
dom f = (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
then A46: dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) c= dom f by XBOOLE_1:7;
assume A47: x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis:
then [x,((id { k where k is Element of NAT : ( k in y & k < i ) } ) . x)] in id { k where k is Element of NAT : ( k in y & k < i ) } by FUNCT_1:def 2;
hence f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x by A47, A46, A45, FUNCT_1:def 2; :: thesis:

end;

reconsider f2 = f2 as Function by A40, FUNCT_1:def 1;
assume A48: not i in y ; :: thesis:

A49: now :: thesis:

let z be object ; :: thesis:
set k = z;
assume A50: z in y9 ; :: thesis:
then z in Seg (n + 1) by A1;
then reconsider k = z as Element of NAT ;

per cases ;

suppose k <= i ; :: thesis:

then k < i by A48, A50, XXREAL_0:1;
then z in { k where k is Element of NAT : ( k in y & k < i ) } by A50;
then z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) ;
then z in (rng (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (rng f2) by XBOOLE_0:def 3;
hence z in rng f by RELAT_1:12; :: thesis:

end;

suppose A51: k > i ; :: thesis:

set x99 = k - 1;
[(k - 1),z] in f2 by A50, A51;
then z in rng f2 by XTUPLE_0:def 13;
then z in (rng (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (rng f2) by XBOOLE_0:def 3;
hence z in rng f by RELAT_1:12; :: thesis:

end;

now :: thesis:

let z be object ; :: thesis:
assume z in rng f ; :: thesis:
then A52: z in (rng (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (rng f2) by RELAT_1:12;

per cases by A52, XBOOLE_0:def 3;

suppose z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis:

then z in { k where k is Element of NAT : ( k in y & k < i ) } ;
then ex k being Element of NAT st
( k = z & k in y & k < i ) ;
hence z in y9 ; :: thesis:

end;

suppose z in rng f2 ; :: thesis:

then consider x99 being object such that
A53: [x99,z] in f2 by XTUPLE_0:def 13;
ex k being Element of NAT st
( [(k - 1),k] = [x99,z] & k in y9 & k > i ) by A53;
hence z in y9 by XTUPLE_0:1; :: thesis:

end;

then A54: rng f = y9 by A49, TARSKI:2;

now :: thesis:

let a, b be object ; :: thesis:

hereby :: thesis:

assume A55: [a,b] in f ; :: thesis:

per cases in id { k where k is Element of NAT : ( k in y & k < i ) } or [a,b] in f2 ) by A55, XBOOLE_0:def 3;

suppose A56: [a,b] in id { k where k is Element of NAT : ( k in y & k < i ) } ; :: thesis:

reconsider i9 = i, n9 = n as Element of NAT by ORDINAL1:def 12;
A57: a = b by A56, RELAT_1:def 10;
a in { k where k is Element of NAT : ( k in y & k < i ) } by A56, RELAT_1:def 10;
then consider a9 being Element of NAT such that
A58: a9 = a and
A59: a9 in y and
A60: a9 < i ;
A61: 1 <= a9 by A1, A59, FINSEQ_1:1;
i <= n + 1 by A3, FINSEQ_1:1;
then a9 < n + 1 by A60, XXREAL_0:2;
then a9 <= n by NAT_1:13;
then A62: a in Seg n by A58, A61;
then a in Seg (len (Sgm ((Seg (n + 1)) \ {i}))) by A3, FINSEQ_3:107;
then A63: a in dom (Sgm ((Seg (n + 1)) \ {i})) by FINSEQ_1:def 3;
a9 = (Sgm ((Seg (n9 + 1)) \ {i9})) . a9 by A3, A58, A60, A61, A62, FINSEQ_3:108;
then [a,b] in Sgm ((Seg (n + 1)) \ {i}) by A57, A58, A63, FUNCT_1:1;
hence [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) by A54, A57, A58, A59, RELAT_1:def 12; :: thesis:

end;

suppose A64: [a,b] in f2 ; :: thesis:

reconsider i9 = i, n9 = n as Element of NAT by ORDINAL1:def 12;
consider b9 being Element of NAT such that
A65: [a,b] = [(b9 - 1),b9] and
A66: b9 in y9 and
A67: b9 > i by A64;
A68: a = b9 - 1 by A65, XTUPLE_0:1;
reconsider a9 = b9 - 1 as Integer ;
i + 1 <= b9 by A67, NAT_1:13;
then A69: (i + 1) - 1 <= b9 - 1 by XREAL_1:9;
then A70: 1 <= a9 by A4, XXREAL_0:2;
reconsider a9 = a9 as Element of NAT by A69, INT_1:3;
b9 <= n + 1 by A1, A66, FINSEQ_1:1;
then A71: b9 - 1 <= (n + 1) - 1 by XREAL_1:9;
then A72: a9 in Seg n by A70;
then a in Seg n by A65, XTUPLE_0:1;
then a in Seg (len (Sgm ((Seg (n + 1)) \ {i}))) by A3, FINSEQ_3:107;
then A73: a in dom (Sgm ((Seg (n + 1)) \ {i})) by FINSEQ_1:def 3;
a9 + 1 = (Sgm ((Seg (n9 + 1)) \ {i9})) . a9 by A3, A71, A69, A72, FINSEQ_3:108;
then [a,b] in Sgm ((Seg (n + 1)) \ {i}) by A65, A68, A73, FUNCT_1:1;
hence [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) by A54, A65, A66, RELAT_1:def 12; :: thesis:

end;

assume A74: [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ; :: thesis:
then A75: [a,b] in Sgm ((Seg (n + 1)) \ {i}) by RELAT_1:def 12;
then A76: a in dom (Sgm ((Seg (n + 1)) \ {i})) by XTUPLE_0:def 12;
b in rng f by A74, RELAT_1:def 12;
then b in Seg (n + 1) by A1, A54;
then reconsider a9 = a, b9 = b as Element of NAT by A76;
A77: a in Seg (len (Sgm ((Seg (n + 1)) \ {i}))) by A76, FINSEQ_1:def 3;
then A78: 1 <= a9 by FINSEQ_1:1;
A79: b in y by A54, A74, RELAT_1:def 12;
A80: a in Seg n by A3, A77, FINSEQ_3:107;
reconsider i = i, n = n as Element of NAT by ORDINAL1:def 12;
A81: a9 <= n by A80, FINSEQ_1:1;

per cases ;

suppose A82: a9 < i ; :: thesis:

then (Sgm ((Seg (n + 1)) \ {i})) . a9 = a9 by A3, A80, A78, FINSEQ_3:108;
then A83: b = a by A75, FUNCT_1:1;
then a9 in { k where k is Element of NAT : ( k in y & k < i ) } by A79, A82;
then [a,b] in id { k where k is Element of NAT : ( k in y & k < i ) } by A83, RELAT_1:def 10;
hence [a,b] in f by XBOOLE_0:def 3; :: thesis:

end;

suppose A84: i <= a9 ; :: thesis:

then (Sgm ((Seg (n + 1)) \ {i})) . a9 = a9 + 1 by A3, A80, A81, FINSEQ_3:108;
then A85: b9 = a9 + 1 by A75, FUNCT_1:1;
then A86: b9 > i by A84, NAT_1:13;
A87: a = b9 - 1 by A85;
b9 in y9 by A54, A74, RELAT_1:def 12;
then [a,b] in f2 by A86, A87;
hence [a,b] in f by XBOOLE_0:def 3; :: thesis:

end;

then A88: f = (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ;
reconsider g = f " as PartFunc of (dom (f ")),(rng (f ")) by RELSET_1:4;

A89: now :: thesis:

let x be set ; :: thesis:
A90: f2 c= f by XBOOLE_1:7;
dom f = (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
then A91: dom f2 c= dom f by XBOOLE_1:7;
assume A92: x in dom f2 ; :: thesis:
then [x,(f2 . x)] in f2 by FUNCT_1:def 2;
hence f . x = f2 . x by A92, A91, A90, FUNCT_1:def 2; :: thesis:

end;

now :: thesis:

let y1, y2 be object ; :: thesis:
assume y1 in dom f ; :: thesis:
then A93: y1 in (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
assume y2 in dom f ; :: thesis:
then A94: y2 in (dom (id { k where k is Element of NAT : ( k in y & k < i ) } )) \/ (dom f2) by XTUPLE_0:23;
assume A95: f . y1 = f . y2 ; :: thesis:

per cases by A93, XBOOLE_0:def 3;

suppose A96: y1 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis:

then A97: (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y1 = y1 by FUNCT_1:17;
then A98: f . y1 = y1 by A44, A96;

per cases by A94, XBOOLE_0:def 3;

suppose A99: y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis:

then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y2 = y2 by FUNCT_1:17;
hence y1 = y2 by A44, A95, A98, A99; :: thesis:

end;

suppose A100: y2 in dom f2 ; :: thesis:

then f . y2 = f2 . y2 by A89;
then [y2,(f . y2)] in f2 by A100, FUNCT_1:def 2;
then A101: ex k being Element of NAT st
( [(k - 1),k] = [y2,(f . y2)] & k in y9 & k > i ) ;
f . y1 = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y1 by A44, A96;
then f . y1 in { k where k is Element of NAT : ( k in y & k < i ) } by A96, A97;
then ex k9 being Element of NAT st
( k9 = f . y1 & k9 in y & k9 < i ) ;
hence y1 = y2 by A95, A101, XTUPLE_0:1; :: thesis:

end;

suppose A102: y1 in dom f2 ; :: thesis:

then f . y1 = f2 . y1 by A89;
then [y1,(f . y1)] in f2 by A102, FUNCT_1:def 2;
then consider k being Element of NAT such that
A103: [(k - 1),k] = [y1,(f . y1)] and
k in y9 and
A104: k > i ;
A105: k = f . y1 by A103, XTUPLE_0:1;

per cases by A94, XBOOLE_0:def 3;

suppose A106: y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) ; :: thesis:

then (id { k where k is Element of NAT : ( k in y & k < i ) } ) . y2 = y2 by FUNCT_1:17;
then f . y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) by A44, A106;
then f . y2 in { k where k is Element of NAT : ( k in y & k < i ) } ;
then ex k9 being Element of NAT st
( k9 = f . y2 & k9 in y & k9 < i ) ;
hence y1 = y2 by A95, A103, A104, XTUPLE_0:1; :: thesis:

end;

suppose A107: y2 in dom f2 ; :: thesis:

then f . y2 = f2 . y2 by A89;
then [y2,(f . y2)] in f2 by A107, FUNCT_1:def 2;
then consider k being Element of NAT such that
A108: [(k - 1),k] = [y2,(f . y2)] and
k in y9 and
k > i ;
k = f . y2 by A108, XTUPLE_0:1;
hence y1 = y2 by A95, A103, A105, A108, XTUPLE_0:1; :: thesis:

end;

then A109: f is one-to-one by FUNCT_1:def 4;
then f " = f ~ by FUNCT_1:def 5;
then A110: f " = ((Sgm ((Seg (n + 1)) \ {i})) ~) | (dom (f ")) by A88, Lm35;
dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) = { k where k is Element of NAT : ( k in y & k < i ) } ;
then A111: dom f = x9 by A21, XTUPLE_0:23;
then dom f c= NAT by A14, XBOOLE_1:1;
then rng g c= NAT by A109, FUNCT_1:33;
then A112: rng g c= REAL by NUMBERS:19;
rng f c= NAT by A1, A54, XBOOLE_1:1;
then dom g c= NAT by A109, FUNCT_1:33;
then dom g c= REAL by NUMBERS:19;
then reconsider g = g as PartFunc of REAL,REAL by A112, RELSET_1:7;
A113: dom (f ") = y by A109, A54, FUNCT_1:33;

now :: thesis:

let r1, r2 be Real; :: thesis:
A114: g = ((id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2) ~ by A109, FUNCT_1:def 5
.= ((id { k where k is Element of NAT : ( k in y & k < i ) } ) ~) \/ (f2 ~) by RELAT_1:23 ;
assume r1 in y /\ (dom g) ; :: thesis:
then A115: [r1,(g . r1)] in g by A113, FUNCT_1:1;
assume r2 in y /\ (dom g) ; :: thesis:
then A116: [r2,(g . r2)] in g by A113, FUNCT_1:1;
assume A117: r1 < r2 ; :: thesis:

per cases in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ or [r1,(g . r1)] in f2 ~ ) by A115, A114, XBOOLE_0:def 3;

suppose [r1,(g . r1)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ ; :: thesis:

then A118: [r1,(g . r1)] in id { k where k is Element of NAT : ( k in y & k < i ) } ;
then A119: r1 = g . r1 by RELAT_1:def 10;
r1 in { k where k is Element of NAT : ( k in y & k < i ) } by A118, RELAT_1:def 10;
then A120: ex k9 being Element of NAT st
( g . r1 = k9 & k9 in y & k9 < i ) by A119;

per cases in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ or [r2,(g . r2)] in f2 ~ ) by A116, A114, XBOOLE_0:def 3;

suppose [r2,(g . r2)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ ; :: thesis:

then [r2,(g . r2)] in id { k where k is Element of NAT : ( k in y & k < i ) } ;
hence g . r1 < g . r2 by A117, A119, RELAT_1:def 10; :: thesis:

end;

suppose [r2,(g . r2)] in f2 ~ ; :: thesis:

then [(g . r2),r2] in f2 by RELAT_1:def 7;
then consider k99 being Element of NAT such that
A121: [(k99 - 1),k99] = [(g . r2),r2] and
k99 in y9 and
A122: k99 > i ;
reconsider k999 = g . r2, i9 = i - 1 as Integer by A121, XTUPLE_0:1;
k99 - 1 = g . r2 by A121, XTUPLE_0:1;
then i - 1 < g . r2 by A122, XREAL_1:9;
then i9 + 1 <= k999 by INT_1:7;
hence g . r1 < g . r2 by A120, XXREAL_0:2; :: thesis:

end;

suppose [r1,(g . r1)] in f2 ~ ; :: thesis:

then [(g . r1),r1] in f2 by RELAT_1:def 7;
then consider k9 being Element of NAT such that
A123: [(k9 - 1),k9] = [(g . r1),r1] and
k9 in y9 and
A124: k9 > i ;
A125: k9 - 1 = g . r1 by A123, XTUPLE_0:1;
A126: r1 = k9 by A123, XTUPLE_0:1;

per cases in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ or [r2,(g . r2)] in f2 ~ ) by A116, A114, XBOOLE_0:def 3;

suppose [r2,(g . r2)] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) ~ ; :: thesis:

then [r2,(g . r2)] in id { k where k is Element of NAT : ( k in y & k < i ) } ;
then r2 in { k where k is Element of NAT : ( k in y & k < i ) } by RELAT_1:def 10;
then ex k99 being Element of NAT st
( r2 = k99 & k99 in y & k99 < i ) ;
hence g . r1 < g . r2 by A117, A124, A126, XXREAL_0:2; :: thesis:

end;

suppose [r2,(g . r2)] in f2 ~ ; :: thesis:

then [(g . r2),r2] in f2 by RELAT_1:def 7;
then consider k99 being Element of NAT such that
A127: [(k99 - 1),k99] = [(g . r2),r2] and
k99 in y9 and
k99 > i ;
( k99 - 1 = g . r2 & r2 = k99 ) by A127, XTUPLE_0:1;
hence g . r1 < g . r2 by A117, A125, A126, XREAL_1:9; :: thesis:

end;

then A128: g | y is increasing by RFUNCT_2:20;
A129: rng (f ") = { k where k is Element of NAT : ( k in y & k i ) } by A109, A111, FUNCT_1:33;
then A130: { k where k is Element of NAT : ( k in y & k i ) } = (f ") .: y by A113, RELAT_1:113;

now :: thesis:

let x9 be object ; :: thesis:
assume A131: x9 in g .: y ; :: thesis:
then not x9 = 0 by A14, A130, FINSEQ_1:1;
then A132: not x9 in {0} by TARSKI:def 1;
x9 in Seg n by A6, A130, A131;
hence x9 in NAT \ {0} by A132, XBOOLE_0:def 5; :: thesis:

end;

then A133: g .: y c= NAT \ {0} ;
take { k where k is Element of NAT : ( k in y & k i ) } ; :: thesis:
Sgm ((Seg (n + 1)) \ {i}) is one-to-one by FINSEQ_3:92, XBOOLE_1:36;
then A134: (Sgm ((Seg (n + 1)) \ {i})) " = (Sgm ((Seg (n + 1)) \ {i})) ~ by FUNCT_1:def 5;
Sgm ( { k where k is Element of NAT : ( k in y & k i ) } ) = Sgm (g .: y) by A113, A129, RELAT_1:113
.= (((Sgm ((Seg (n + 1)) \ {i})) ") | y) * (Sgm y) by A1, A113, A128, A133, A134, A110, Lm37
.= ((Sgm ((Seg (n + 1)) \ {i})) ") * (y |` (Sgm y)) by Lm36
.= ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) by A2 ;
hence Sgm ( { k where k is Element of NAT : ( k in y & k i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) ; :: thesis:
thus { k where k is Element of NAT : ( k in y & k i ) } c= Seg n by A6; :: thesis: