let y be set ; :: thesis: for i, n being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds

ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )

let i, n be Nat; :: thesis: ( y c= Seg (n + 1) & i in Seg (n + 1) & not i in y implies ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )

set x1 = { k where k is Element of NAT : ( k in y & k < i ) } ;

set x2 = { (k - 1) 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 ) } \/ { (k - 1) 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: ( not i in Seg (n + 1) or i in y or ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )

then A2: y = rng (Sgm y) by FINSEQ_1:def 13;

assume A3: i in Seg (n + 1) ; :: thesis: ( i in y or ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )

then A4: 1 <= i by FINSEQ_1:1;

A5: i <= n + 1 by A3, FINSEQ_1:1;

then reconsider x9 = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) 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 ) } ;

set f = (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2;

assume A48: not i in y ; :: thesis: ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )

reconsider g = f " as PartFunc of (dom (f ")),(rng (f ")) by RELSET_1: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;

A129: rng (f ") = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) 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 ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } = (f ") .: y by A113, RELAT_1:113;

take { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: ( Sgm ( { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n )

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 ) } \/ { (k - 1) 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 ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) ; :: thesis: { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n

thus { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n by A6; :: thesis: verum

ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )

let i, n be Nat; :: thesis: ( y c= Seg (n + 1) & i in Seg (n + 1) & not i in y implies ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )

set x1 = { k where k is Element of NAT : ( k in y & k < i ) } ;

set x2 = { (k - 1) 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 ) } \/ { (k - 1) 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: ( not i in Seg (n + 1) or i in y or ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )

then A2: y = rng (Sgm y) by FINSEQ_1:def 13;

assume A3: i in Seg (n + 1) ; :: thesis: ( i in y or ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) )

then A4: 1 <= i by FINSEQ_1:1;

A5: i <= n + 1 by A3, FINSEQ_1:1;

A6: now :: thesis: for z being object st z in { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } holds

z in Seg n

then A14:
{ k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n
;z in Seg n

let z be object ; :: thesis: ( z in { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } implies b_{1} in Seg n )

assume A7: z in { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: b_{1} in Seg n

end;assume A7: z in { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: b

per cases
( z in { k where k is Element of NAT : ( k in y & k < i ) } or z in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } )
by A7, XBOOLE_0:def 3;

end;

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

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: verum

end;( 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: verum

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

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: verum

end;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: verum

then reconsider x9 = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) 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: for x being object st x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } holds

ex y, z being object st x = [y,z]

then reconsider f2 = { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } as Relation by RELAT_1:def 1;ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } implies ex y, z being object st x = [y,z] )

assume x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } ; :: thesis: ex y, z being object st x = [y,z]

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: ex z being object st x = [y,z]

take z = z; :: thesis: x = [y,z]

thus x = [y,z] by A15; :: thesis: verum

end;assume x in { [(k - 1),k] where k is Element of NAT : ( k in y9 & k > i ) } ; :: thesis: ex y, z being object st x = [y,z]

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: ex z being object st x = [y,z]

take z = z; :: thesis: x = [y,z]

thus x = [y,z] by A15; :: thesis: verum

set f = (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2;

A16: now :: thesis: for x being object st x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } holds

x in dom f2

x in dom f2

let x be object ; :: thesis: ( x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } implies x in dom f2 )

assume x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: x in dom f2

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: verum

end;assume x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: x in dom f2

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: verum

now :: thesis: for x being object st x in dom f2 holds

x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) }

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

let x be object ; :: thesis: ( x in dom f2 implies x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) } )

assume x in dom f2 ; :: thesis: x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) }

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: verum

end;assume x in dom f2 ; :: thesis: x in { (k - 1) where k is Element of NAT : ( k in y & k > i ) }

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: verum

A22: now :: thesis: for x, y1, y2 being object st [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 & [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 holds

y1 = y2

y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 & [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 implies b_{2} = b_{3} )

assume A23: [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis: ( [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 implies b_{2} = b_{3} )

assume A24: [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis: b_{2} = b_{3}

A25: ( y1 is set & y2 is set ) by TARSKI:1;

end;assume A23: [x,y1] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis: ( [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 implies b

assume A24: [x,y2] in (id { k where k is Element of NAT : ( k in y & k < i ) } ) \/ f2 ; :: thesis: b

A25: ( y1 is set & y2 is set ) by TARSKI:1;

per cases
( [x,y1] 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;

end;

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

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;

end;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
( [x,y2] 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;

end;

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

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: verum

end;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: verum

suppose A31:
[x,y2] in f2
; :: thesis: b_{2} = b_{3}

x in { k where k is Element of NAT : ( k in y & k < i ) }
by A27;

then consider k9 being Element of NAT such that

A32: k9 = x and

k9 in y and

A33: k9 < i ;

x in { (k - 1) 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: verum

end;then consider k9 being Element of NAT such that

A32: k9 = x and

k9 in y and

A33: k9 < i ;

x in { (k - 1) 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: verum

suppose
[x,y1] in f2
; :: thesis: b_{2} = b_{3}

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;

end;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
( [x,y2] 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;

end;

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

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

then consider k9 being Element of NAT such that

A37: k9 = x and

k9 in y and

A38: k9 < i ;

k9 = k - 1 by A34, A37, XTUPLE_0:1;

then k9 + 1 > i by A35;

hence y1 = y2 by A38, NAT_1:13; :: thesis: verum

end;then x in { k where k is Element of NAT : ( k in y & k < i ) } ;

then consider k9 being Element of NAT such that

A37: k9 = x and

k9 in y and

A38: k9 < i ;

k9 = k - 1 by A34, A37, XTUPLE_0:1;

then k9 + 1 > i by A35;

hence y1 = y2 by A38, NAT_1:13; :: thesis: verum

A40: now :: thesis: for x, y1, y2 being object st [x,y1] in f2 & [x,y2] in f2 holds

y1 = y2

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

let x, y1, y2 be object ; :: thesis: ( [x,y1] in f2 & [x,y2] in f2 implies y1 = y2 )

assume [x,y1] in f2 ; :: thesis: ( [x,y2] in f2 implies y1 = y2 )

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: y1 = y2

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: verum

end;assume [x,y1] in f2 ; :: thesis: ( [x,y2] in f2 implies y1 = y2 )

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: y1 = y2

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: verum

A44: now :: thesis: for x being object st x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) holds

f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x

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

let x be object ; :: thesis: ( x in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) implies f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x )

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: f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x

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: verum

end;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: f . x = (id { k where k is Element of NAT : ( k in y & k < i ) } ) . x

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: verum

assume A48: not i in y ; :: thesis: ex x being set st

( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )

A49: now :: thesis: for z being object st z in y9 holds

z in rng f

z in rng f

let z be object ; :: thesis: ( z in y9 implies b_{1} in rng f )

set k = z;

assume A50: z in y9 ; :: thesis: b_{1} in rng f

then z in Seg (n + 1) by A1;

then reconsider k = z as Element of NAT ;

end;set k = z;

assume A50: z in y9 ; :: thesis: b

then z in Seg (n + 1) by A1;

then reconsider k = z as Element of NAT ;

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

end;

suppose
k <= i
; :: thesis: b_{1} in rng f

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: verum

end;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: verum

now :: thesis: for z being object st z in rng f holds

z in y9

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

let z be object ; :: thesis: ( z in rng f implies b_{1} in y9 )

assume z in rng f ; :: thesis: b_{1} in y9

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

end;assume z in rng f ; :: thesis: b

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
( z in rng (id { k where k is Element of NAT : ( k in y & k < i ) } ) or z in rng f2 )
by A52, XBOOLE_0:def 3;

end;

now :: thesis: for a, b being object holds

( ( [a,b] in f implies [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ) & ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [a,b] in f ) )

then A88:
f = (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))
;( ( [a,b] in f implies [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ) & ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [a,b] in f ) )

let a, b be object ; :: thesis: ( ( [a,b] in f implies [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) ) & ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [b_{1},b_{2}] in f ) )

_{1},b_{2}] in f

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;

end;hereby :: thesis: ( [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i})) implies [b_{1},b_{2}] in f )

assume A74:
[a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))
; :: thesis: [bassume A55:
[a,b] in f
; :: thesis: [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))

end;per cases
( [a,b] 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;

end;

suppose A56:
[a,b] in id { k where k is Element of NAT : ( k in y & k < i ) }
; :: thesis: [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))

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: verum

end;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: verum

suppose A64:
[a,b] in f2
; :: thesis: [a,b] in (rng f) |` (Sgm ((Seg (n + 1)) \ {i}))

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: verum

end;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: verum

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
( a9 < i or i <= a9 )
;

end;

suppose A82:
a9 < i
; :: thesis: [b_{1},b_{2}] in f

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: verum

end;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: verum

suppose A84:
i <= a9
; :: thesis: [b_{1},b_{2}] in f

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: verum

end;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: verum

reconsider g = f " as PartFunc of (dom (f ")),(rng (f ")) by RELSET_1:4;

A89: now :: thesis: for x being set st x in dom f2 holds

f . x = f2 . x

f . x = f2 . x

let x be set ; :: thesis: ( x in dom f2 implies f . x = f2 . x )

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: f . x = f2 . x

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: verum

end;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: f . x = f2 . x

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: verum

now :: thesis: for y1, y2 being object st y1 in dom f & y2 in dom f & f . y1 = f . y2 holds

y1 = y2

then A109:
f is one-to-one
by FUNCT_1:def 4;y1 = y2

let y1, y2 be object ; :: thesis: ( y1 in dom f & y2 in dom f & f . y1 = f . y2 implies b_{1} = b_{2} )

assume y1 in dom f ; :: thesis: ( y2 in dom f & f . y1 = f . y2 implies b_{1} = b_{2} )

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: ( f . y1 = f . y2 implies b_{1} = b_{2} )

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: b_{1} = b_{2}

end;assume y1 in dom f ; :: thesis: ( y2 in dom f & f . y1 = f . y2 implies b

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: ( f . y1 = f . y2 implies b

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: b

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

end;

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

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;

end;then A98: f . y1 = y1 by A44, A96;

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

end;

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

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: verum

end;hence y1 = y2 by A44, A95, A98, A99; :: thesis: verum

suppose A100:
y2 in dom f2
; :: thesis: b_{1} = b_{2}

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: verum

end;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: verum

suppose A102:
y1 in dom f2
; :: thesis: b_{1} = b_{2}

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;

end;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
( y2 in dom (id { k where k is Element of NAT : ( k in y & k < i ) } ) or y2 in dom f2 )
by A94, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

suppose A107:
y2 in dom f2
; :: thesis: b_{1} = b_{2}

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: verum

end;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: verum

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: for r1, r2 being Real st r1 in y /\ (dom g) & r2 in y /\ (dom g) & r1 < r2 holds

g . r1 < g . r2

then A128:
g | y is increasing
by RFUNCT_2:20;g . r1 < g . r2

let r1, r2 be Real; :: thesis: ( r1 in y /\ (dom g) & r2 in y /\ (dom g) & r1 < r2 implies g . b_{1} < g . b_{2} )

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: ( r2 in y /\ (dom g) & r1 < r2 implies g . b_{1} < g . b_{2} )

then A115: [r1,(g . r1)] in g by A113, FUNCT_1:1;

assume r2 in y /\ (dom g) ; :: thesis: ( r1 < r2 implies g . b_{1} < g . b_{2} )

then A116: [r2,(g . r2)] in g by A113, FUNCT_1:1;

assume A117: r1 < r2 ; :: thesis: g . b_{1} < g . b_{2}

end;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: ( r2 in y /\ (dom g) & r1 < r2 implies g . b

then A115: [r1,(g . r1)] in g by A113, FUNCT_1:1;

assume r2 in y /\ (dom g) ; :: thesis: ( r1 < r2 implies g . b

then A116: [r2,(g . r2)] in g by A113, FUNCT_1:1;

assume A117: r1 < r2 ; :: thesis: g . b

per cases
( [r1,(g . r1)] 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;

end;

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

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;

end;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
( [r2,(g . r2)] 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;

end;

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

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: verum

end;hence g . r1 < g . r2 by A117, A119, RELAT_1:def 10; :: thesis: verum

suppose
[r2,(g . r2)] in f2 ~
; :: thesis: g . b_{1} < g . b_{2}

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: verum

end;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: verum

suppose
[r1,(g . r1)] in f2 ~
; :: thesis: g . b_{1} < g . b_{2}

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;

end;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
( [r2,(g . r2)] 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;

end;

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

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: verum

end;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: verum

suppose
[r2,(g . r2)] in f2 ~
; :: thesis: g . b_{1} < g . b_{2}

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: verum

end;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: verum

A129: rng (f ") = { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) 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 ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } = (f ") .: y by A113, RELAT_1:113;

now :: thesis: for x9 being object st x9 in g .: y holds

x9 in NAT \ {0}

then A133:
g .: y c= NAT \ {0}
;x9 in NAT \ {0}

let x9 be object ; :: thesis: ( x9 in g .: y implies x9 in NAT \ {0} )

assume A131: x9 in g .: y ; :: thesis: x9 in NAT \ {0}

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: verum

end;assume A131: x9 in g .: y ; :: thesis: x9 in NAT \ {0}

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: verum

take { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ; :: thesis: ( Sgm ( { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n )

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 ) } \/ { (k - 1) 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 ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } ) = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) ; :: thesis: { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n

thus { k where k is Element of NAT : ( k in y & k < i ) } \/ { (k - 1) where k is Element of NAT : ( k in y & k > i ) } c= Seg n by A6; :: thesis: verum