let O be set ; :: thesis: for G being GroupWithOperators of O

for s1, s19, s2 being CompositionSeries of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds

s19 is_finer_than s2

let G be GroupWithOperators of O; :: thesis: for s1, s19, s2 being CompositionSeries of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds

s19 is_finer_than s2

let s1, s19, s2 be CompositionSeries of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds

s19 is_finer_than s2

let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 implies s19 is_finer_than s2 )

assume that

A1: i in dom s1 and

A2: i + 1 in dom s1 ; :: thesis: ( not s1 . i = s1 . (i + 1) or not s19 = Del (s1,i) or not s2 is jordan_holder or not s1 is_finer_than s2 or s19 is_finer_than s2 )

A3: i in Seg (len s1) by A1, FINSEQ_1:def 3;

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

set k = (len s1) - 1;

assume A5: s1 . i = s1 . (i + 1) ; :: thesis: ( not s19 = Del (s1,i) or not s2 is jordan_holder or not s1 is_finer_than s2 or s19 is_finer_than s2 )

reconsider k = (len s1) - 1 as Integer ;

assume A6: s19 = Del (s1,i) ; :: thesis: ( not s2 is jordan_holder or not s1 is_finer_than s2 or s19 is_finer_than s2 )

assume A7: s2 is jordan_holder ; :: thesis: ( not s1 is_finer_than s2 or s19 is_finer_than s2 )

i <= len s1 by A3, FINSEQ_1:1;

then 1 <= len s1 by A4, XXREAL_0:2;

then 1 - 1 <= (len s1) - 1 by XREAL_1:9;

then reconsider k = k as Element of NAT by INT_1:3;

A8: dom s1 = Seg (k + 1) by FINSEQ_1:def 3;

assume s1 is_finer_than s2 ; :: thesis: s19 is_finer_than s2

then consider z being set such that

A9: z c= dom s1 and

A10: s2 = s1 * (Sgm z) ;

A11: i + 1 in Seg (len s1) by A2, FINSEQ_1:def 3;

A96: y c= Seg (k + 1) and

A97: not i in y and

A98: s2 = s1 * (Sgm y) ;

for s1, s19, s2 being CompositionSeries of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds

s19 is_finer_than s2

let G be GroupWithOperators of O; :: thesis: for s1, s19, s2 being CompositionSeries of G

for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds

s19 is_finer_than s2

let s1, s19, s2 be CompositionSeries of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds

s19 is_finer_than s2

let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 implies s19 is_finer_than s2 )

assume that

A1: i in dom s1 and

A2: i + 1 in dom s1 ; :: thesis: ( not s1 . i = s1 . (i + 1) or not s19 = Del (s1,i) or not s2 is jordan_holder or not s1 is_finer_than s2 or s19 is_finer_than s2 )

A3: i in Seg (len s1) by A1, FINSEQ_1:def 3;

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

set k = (len s1) - 1;

assume A5: s1 . i = s1 . (i + 1) ; :: thesis: ( not s19 = Del (s1,i) or not s2 is jordan_holder or not s1 is_finer_than s2 or s19 is_finer_than s2 )

reconsider k = (len s1) - 1 as Integer ;

assume A6: s19 = Del (s1,i) ; :: thesis: ( not s2 is jordan_holder or not s1 is_finer_than s2 or s19 is_finer_than s2 )

assume A7: s2 is jordan_holder ; :: thesis: ( not s1 is_finer_than s2 or s19 is_finer_than s2 )

i <= len s1 by A3, FINSEQ_1:1;

then 1 <= len s1 by A4, XXREAL_0:2;

then 1 - 1 <= (len s1) - 1 by XREAL_1:9;

then reconsider k = k as Element of NAT by INT_1:3;

A8: dom s1 = Seg (k + 1) by FINSEQ_1:def 3;

assume s1 is_finer_than s2 ; :: thesis: s19 is_finer_than s2

then consider z being set such that

A9: z c= dom s1 and

A10: s2 = s1 * (Sgm z) ;

A11: i + 1 in Seg (len s1) by A2, FINSEQ_1:def 3;

now :: thesis: ex y being set st

( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )end;

then consider y being set such that ( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

per cases
( not i in z or i in z )
;

end;

suppose A12:
not i in z
; :: thesis: ex y being set st

( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

set y = z;

take y = z; :: thesis: ( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

thus y c= Seg (k + 1) by A9, FINSEQ_1:def 3; :: thesis: ( not i in y & s2 = s1 * (Sgm y) )

thus not i in y by A12; :: thesis: s2 = s1 * (Sgm y)

thus s2 = s1 * (Sgm y) by A10; :: thesis: verum

end;take y = z; :: thesis: ( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

thus y c= Seg (k + 1) by A9, FINSEQ_1:def 3; :: thesis: ( not i in y & s2 = s1 * (Sgm y) )

thus not i in y by A12; :: thesis: s2 = s1 * (Sgm y)

thus s2 = s1 * (Sgm y) by A10; :: thesis: verum

suppose A13:
i in z
; :: thesis: ex y being set st

( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

then A16: {(i + 1)} misses {i} by XBOOLE_0:def 7;

reconsider y = (z \/ {(i + 1)}) \ {i} as set ;

take y = y; :: thesis: ( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

{(i + 1)} c= Seg (k + 1) by A11, ZFMISC_1:31;

then A17: z \/ {(i + 1)} c= Seg (k + 1) by A9, A8, XBOOLE_1:8;

hence A18: y c= Seg (k + 1) ; :: thesis: ( not i in y & s2 = s1 * (Sgm y) )

then y c= dom s1 by FINSEQ_1:def 3;

then A19: rng (Sgm y) c= dom s1 by A18, FINSEQ_1:def 13;

reconsider y9 = y, z = z as finite set by A9;

A20: dom (Sgm y9) = Seg (card y9) by A17, FINSEQ_3:40, XBOOLE_1:1;

i in z \/ {(i + 1)} by A13, XBOOLE_0:def 3;

then {i} c= z \/ {(i + 1)} by ZFMISC_1:31;

then card ((z \/ {(i + 1)}) \ {i}) = (card (z \/ {(i + 1)})) - (card {i}) by CARD_2:44;

then A21: card y9 = (card (z \/ {(i + 1)})) - 1 by CARD_1:30;

then A39: dom (Sgm y9) = dom (Sgm z) by A9, A8, A21, A20, FINSEQ_3:40;

set z2 = { x where x is Element of NAT : ( x in z & i + 1 < x ) } ;

set z1 = { x where x is Element of NAT : ( x in z & x < i ) } ;

then { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= z by XBOOLE_1:7;

then A46: { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= Seg (k + 1) by A42;

{ x where x is Element of NAT : ( x in z & x < i ) } c= z by A45, XBOOLE_1:7, XBOOLE_1:11;

then A47: { x where x is Element of NAT : ( x in z & x < i ) } c= Seg (k + 1) by A42;

then A51: { x where x is Element of NAT : ( x in z & i + 1 < x ) } misses {i} by XBOOLE_0:def 7;

then A54: { x where x is Element of NAT : ( x in z & x < i ) } misses {i} by XBOOLE_0:def 7;

A55: y = ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)}) \ {i} by A43, A40, TARSKI:2

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \ {i}) \/ ({(i + 1)} \ {i}) by XBOOLE_1:42

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \ {i}) \/ {(i + 1)} by A16, XBOOLE_1:83

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \ {i}) \/ ( { x where x is Element of NAT : ( x in z & i + 1 < x ) } \ {i})) \/ {(i + 1)} by XBOOLE_1:42

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by A51, XBOOLE_1:83

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \ {i}) \/ ({i} \ {i})) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by XBOOLE_1:42

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \ {i}) \/ {}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by XBOOLE_1:37

.= (( { x where x is Element of NAT : ( x in z & x < i ) } \/ {}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by A54, XBOOLE_1:83

.= ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } by XBOOLE_1:4 ;

then {(i + 1)} c= y by XBOOLE_1:7, XBOOLE_1:11;

then A56: {(i + 1)} c= Seg (k + 1) by A18;

{ x where x is Element of NAT : ( x in z & i + 1 < x ) } c= y by A55, XBOOLE_1:7;

then A57: { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= Seg (k + 1) by A18;

then { x where x is Element of NAT : ( x in z & x < i ) } c= Seg (k + 1) by A18;

then A69: Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)}) = (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ (Sgm {(i + 1)}) by A56, A66, FINSEQ_3:42;

{ x where x is Element of NAT : ( x in z & x < i ) } \/ {i} c= z by A45, XBOOLE_1:7;

then { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} c= Seg (k + 1) by A42;

then A70: Sgm z = (Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i})) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A45, A46, A58, FINSEQ_3:42;

{i} c= z by A45, XBOOLE_1:7, XBOOLE_1:11;

then {i} c= Seg (k + 1) by A42;

then A71: Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) = (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ (Sgm {i}) by A47, A61, FINSEQ_3:42;

then A72: Sgm z = ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A4, A70, FINSEQ_3:44;

{ x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} c= y by A55, XBOOLE_1:7;

then { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} c= Seg (k + 1) by A18;

then A73: Sgm y = (Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)})) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A55, A57, A63, FINSEQ_3:42;

then A74: Sgm y = ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A69, FINSEQ_3:44;

then A89: dom (s1 * (Sgm z)) = dom (Sgm z) by RELAT_1:27;

then A90: dom (s1 * (Sgm y)) = dom (s1 * (Sgm z)) by A39, A19, RELAT_1:27;

end;

( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

now :: thesis: for x being object holds not x in {(i + 1)} /\ {i}

then
{(i + 1)} /\ {i} = {}
by XBOOLE_0:def 1;let x be object ; :: thesis: not x in {(i + 1)} /\ {i}

assume A14: x in {(i + 1)} /\ {i} ; :: thesis: contradiction

then x in {i} by XBOOLE_0:def 4;

then A15: x = i by TARSKI:def 1;

x in {(i + 1)} by A14, XBOOLE_0:def 4;

then x = i + 1 by TARSKI:def 1;

hence contradiction by A15; :: thesis: verum

end;assume A14: x in {(i + 1)} /\ {i} ; :: thesis: contradiction

then x in {i} by XBOOLE_0:def 4;

then A15: x = i by TARSKI:def 1;

x in {(i + 1)} by A14, XBOOLE_0:def 4;

then x = i + 1 by TARSKI:def 1;

hence contradiction by A15; :: thesis: verum

then A16: {(i + 1)} misses {i} by XBOOLE_0:def 7;

reconsider y = (z \/ {(i + 1)}) \ {i} as set ;

take y = y; :: thesis: ( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )

{(i + 1)} c= Seg (k + 1) by A11, ZFMISC_1:31;

then A17: z \/ {(i + 1)} c= Seg (k + 1) by A9, A8, XBOOLE_1:8;

hence A18: y c= Seg (k + 1) ; :: thesis: ( not i in y & s2 = s1 * (Sgm y) )

then y c= dom s1 by FINSEQ_1:def 3;

then A19: rng (Sgm y) c= dom s1 by A18, FINSEQ_1:def 13;

reconsider y9 = y, z = z as finite set by A9;

A20: dom (Sgm y9) = Seg (card y9) by A17, FINSEQ_3:40, XBOOLE_1:1;

i in z \/ {(i + 1)} by A13, XBOOLE_0:def 3;

then {i} c= z \/ {(i + 1)} by ZFMISC_1:31;

then card ((z \/ {(i + 1)}) \ {i}) = (card (z \/ {(i + 1)})) - (card {i}) by CARD_2:44;

then A21: card y9 = (card (z \/ {(i + 1)})) - 1 by CARD_1:30;

A22: now :: thesis: not i + 1 in z

then
card (z \/ {(i + 1)}) = (card z) + 1
by CARD_2:41;A23:
0 + i < 1 + i
by XREAL_1:6;

assume i + 1 in z ; :: thesis: contradiction

then i + 1 in rng (Sgm z) by A9, A8, FINSEQ_1:def 13;

then consider x99 being object such that

A24: x99 in dom (Sgm z) and

A25: i + 1 = (Sgm z) . x99 by FUNCT_1:def 3;

i in rng (Sgm z) by A9, A8, A13, FINSEQ_1:def 13;

then consider x9 being object such that

A26: x9 in dom (Sgm z) and

A27: i = (Sgm z) . x9 by FUNCT_1:def 3;

reconsider x9 = x9, x99 = x99 as Element of NAT by A26, A24;

A28: dom (Sgm z) = Seg (len (Sgm z)) by FINSEQ_1:def 3;

then A29: x9 <= len (Sgm z) by A26, FINSEQ_1:1;

1 <= x99 by A24, A28, FINSEQ_1:1;

then x9 < x99 by A9, A8, A27, A25, A23, A29, FINSEQ_3:41;

then reconsider l = x99 - x9 as Element of NAT by INT_1:5;

end;assume i + 1 in z ; :: thesis: contradiction

then i + 1 in rng (Sgm z) by A9, A8, FINSEQ_1:def 13;

then consider x99 being object such that

A24: x99 in dom (Sgm z) and

A25: i + 1 = (Sgm z) . x99 by FUNCT_1:def 3;

i in rng (Sgm z) by A9, A8, A13, FINSEQ_1:def 13;

then consider x9 being object such that

A26: x9 in dom (Sgm z) and

A27: i = (Sgm z) . x9 by FUNCT_1:def 3;

reconsider x9 = x9, x99 = x99 as Element of NAT by A26, A24;

A28: dom (Sgm z) = Seg (len (Sgm z)) by FINSEQ_1:def 3;

then A29: x9 <= len (Sgm z) by A26, FINSEQ_1:1;

1 <= x99 by A24, A28, FINSEQ_1:1;

then x9 < x99 by A9, A8, A27, A25, A23, A29, FINSEQ_3:41;

then reconsider l = x99 - x9 as Element of NAT by INT_1:5;

per cases
( l = 0 or 0 < l )
;

end;

suppose A30:
0 < l
; :: thesis: contradiction

set x999 = x9 + 1;

0 + 1 < l + 1 by A30, XREAL_1:6;

then (x9 + 1) - x9 <= x99 - x9 by NAT_1:13;

then A31: x9 + 1 <= x99 by XREAL_1:9;

x99 <= len (Sgm z) by A24, A28, FINSEQ_1:1;

then A32: x9 + 1 <= len (Sgm z) by A31, XXREAL_0:2;

A33: ( 1 + x9 > 0 + x9 & 1 <= x9 ) by A26, A28, FINSEQ_1:1, XREAL_1:6;

then 1 <= x9 + 1 by XXREAL_0:2;

then x9 + 1 in dom (Sgm z) by A28, A32;

then reconsider k3 = (Sgm z) . (x9 + 1) as Element of NAT by FINSEQ_2:11;

i < k3 by A9, A8, A27, A33, A32, FINSEQ_1:def 13;

then A34: i + 1 <= k3 by NAT_1:13;

A35: ( ( 1 <= x9 + 1 & x9 + 1 < x99 & x99 <= len (Sgm z) ) or x9 + 1 = x99 ) by A24, A28, A31, A33, FINSEQ_1:1, XXREAL_0:1, XXREAL_0:2;

then A36: x9 + 1 in dom s2 by A2, A9, A10, A8, A24, A25, A34, FINSEQ_1:def 13, FUNCT_1:11;

A37: s2 is strictly_decreasing by A7;

A38: x9 in dom s2 by A1, A10, A26, A27, FUNCT_1:11;

then reconsider H1 = s2 . x9, H2 = s2 . (x9 + 1) as Element of the_stable_subgroups_of G by A36, FINSEQ_2:11;

reconsider H1 = H1, H2 = H2 as StableSubgroup of G by Def11;

reconsider H1 = H1 as GroupWithOperators of O ;

reconsider H2 = H2 as normal StableSubgroup of H1 by A38, A36, Def28;

s2 . x9 = s1 . ((Sgm z) . x9) by A10, A26, FUNCT_1:13

.= s2 . (x9 + 1) by A5, A9, A10, A8, A27, A24, A25, A35, A34, FINSEQ_1:def 13, FUNCT_1:13 ;

then the carrier of H1 = the carrier of H2 ;

then H1 ./. H2 is trivial by Th77;

hence contradiction by A38, A36, A37; :: thesis: verum

end;0 + 1 < l + 1 by A30, XREAL_1:6;

then (x9 + 1) - x9 <= x99 - x9 by NAT_1:13;

then A31: x9 + 1 <= x99 by XREAL_1:9;

x99 <= len (Sgm z) by A24, A28, FINSEQ_1:1;

then A32: x9 + 1 <= len (Sgm z) by A31, XXREAL_0:2;

A33: ( 1 + x9 > 0 + x9 & 1 <= x9 ) by A26, A28, FINSEQ_1:1, XREAL_1:6;

then 1 <= x9 + 1 by XXREAL_0:2;

then x9 + 1 in dom (Sgm z) by A28, A32;

then reconsider k3 = (Sgm z) . (x9 + 1) as Element of NAT by FINSEQ_2:11;

i < k3 by A9, A8, A27, A33, A32, FINSEQ_1:def 13;

then A34: i + 1 <= k3 by NAT_1:13;

A35: ( ( 1 <= x9 + 1 & x9 + 1 < x99 & x99 <= len (Sgm z) ) or x9 + 1 = x99 ) by A24, A28, A31, A33, FINSEQ_1:1, XXREAL_0:1, XXREAL_0:2;

then A36: x9 + 1 in dom s2 by A2, A9, A10, A8, A24, A25, A34, FINSEQ_1:def 13, FUNCT_1:11;

A37: s2 is strictly_decreasing by A7;

A38: x9 in dom s2 by A1, A10, A26, A27, FUNCT_1:11;

then reconsider H1 = s2 . x9, H2 = s2 . (x9 + 1) as Element of the_stable_subgroups_of G by A36, FINSEQ_2:11;

reconsider H1 = H1, H2 = H2 as StableSubgroup of G by Def11;

reconsider H1 = H1 as GroupWithOperators of O ;

reconsider H2 = H2 as normal StableSubgroup of H1 by A38, A36, Def28;

s2 . x9 = s1 . ((Sgm z) . x9) by A10, A26, FUNCT_1:13

.= s2 . (x9 + 1) by A5, A9, A10, A8, A27, A24, A25, A35, A34, FINSEQ_1:def 13, FUNCT_1:13 ;

then the carrier of H1 = the carrier of H2 ;

then H1 ./. H2 is trivial by Th77;

hence contradiction by A38, A36, A37; :: thesis: verum

then A39: dom (Sgm y9) = dom (Sgm z) by A9, A8, A21, A20, FINSEQ_3:40;

set z2 = { x where x is Element of NAT : ( x in z & i + 1 < x ) } ;

set z1 = { x where x is Element of NAT : ( x in z & x < i ) } ;

A40: now :: thesis: for x being object st x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } holds

x in z

A42:
z c= Seg (k + 1)
by A9, FINSEQ_1:def 3;x in z

let x be object ; :: thesis: ( x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies b_{1} in z )

assume x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ; :: thesis: b_{1} in z

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by XBOOLE_0:def 3;

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } or x in {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by XBOOLE_0:def 3;

then consider x9, x99 being Element of NAT such that

A41: ( ( x = x9 & x9 in z & x9 < i ) or x in {i} or ( x = x99 & x99 in z & i + 1 < x99 ) ) ;

end;assume x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ; :: thesis: b

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by XBOOLE_0:def 3;

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } or x in {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by XBOOLE_0:def 3;

then consider x9, x99 being Element of NAT such that

A41: ( ( x = x9 & x9 in z & x9 < i ) or x in {i} or ( x = x99 & x99 in z & i + 1 < x99 ) ) ;

A43: now :: thesis: for x being object st x in z holds

x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) }

then A45:
z = ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) }
by A40, TARSKI:2;x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) }

let x be object ; :: thesis: ( x in z implies x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } )

assume A44: x in z ; :: thesis: x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) }

then x in Seg (k + 1) by A42;

then reconsider x9 = x as Element of NAT ;

( x9 <= i or i + 1 <= x9 ) by NAT_1:13;

then ( x9 < i or x9 = i or i + 1 < x9 ) by A22, A44, XXREAL_0:1;

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } or x in {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A44, TARSKI:def 1;

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by XBOOLE_0:def 3;

hence x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } by XBOOLE_0:def 3; :: thesis: verum

end;assume A44: x in z ; :: thesis: x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) }

then x in Seg (k + 1) by A42;

then reconsider x9 = x as Element of NAT ;

( x9 <= i or i + 1 <= x9 ) by NAT_1:13;

then ( x9 < i or x9 = i or i + 1 < x9 ) by A22, A44, XXREAL_0:1;

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } or x in {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A44, TARSKI:def 1;

then ( x in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} or x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by XBOOLE_0:def 3;

hence x in ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } by XBOOLE_0:def 3; :: thesis: verum

then { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= z by XBOOLE_1:7;

then A46: { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= Seg (k + 1) by A42;

{ x where x is Element of NAT : ( x in z & x < i ) } c= z by A45, XBOOLE_1:7, XBOOLE_1:11;

then A47: { x where x is Element of NAT : ( x in z & x < i ) } c= Seg (k + 1) by A42;

now :: thesis: for x being object holds not x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i}

then
{ x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i} = {}
by XBOOLE_0:def 1;let x be object ; :: thesis: not x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i}

assume A48: x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i} ; :: thesis: contradiction

then x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } by XBOOLE_0:def 4;

then consider x9 being Element of NAT such that

A49: x9 = x and

x9 in z and

A50: i + 1 < x9 ;

x in {i} by A48, XBOOLE_0:def 4;

then x9 = i by A49, TARSKI:def 1;

then (i + 1) - i < i - i by A50, XREAL_1:9;

then 1 < 0 ;

hence contradiction ; :: thesis: verum

end;assume A48: x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i} ; :: thesis: contradiction

then x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } by XBOOLE_0:def 4;

then consider x9 being Element of NAT such that

A49: x9 = x and

x9 in z and

A50: i + 1 < x9 ;

x in {i} by A48, XBOOLE_0:def 4;

then x9 = i by A49, TARSKI:def 1;

then (i + 1) - i < i - i by A50, XREAL_1:9;

then 1 < 0 ;

hence contradiction ; :: thesis: verum

then A51: { x where x is Element of NAT : ( x in z & i + 1 < x ) } misses {i} by XBOOLE_0:def 7;

now :: thesis: for x being object holds not x in { x where x is Element of NAT : ( x in z & x < i ) } /\ {i}

then
{ x where x is Element of NAT : ( x in z & x < i ) } /\ {i} = {}
by XBOOLE_0:def 1;let x be object ; :: thesis: not x in { x where x is Element of NAT : ( x in z & x < i ) } /\ {i}

assume A52: x in { x where x is Element of NAT : ( x in z & x < i ) } /\ {i} ; :: thesis: contradiction

then x in { x where x is Element of NAT : ( x in z & x < i ) } by XBOOLE_0:def 4;

then A53: ex x9 being Element of NAT st

( x9 = x & x9 in z & x9 < i ) ;

x in {i} by A52, XBOOLE_0:def 4;

hence contradiction by A53, TARSKI:def 1; :: thesis: verum

end;assume A52: x in { x where x is Element of NAT : ( x in z & x < i ) } /\ {i} ; :: thesis: contradiction

then x in { x where x is Element of NAT : ( x in z & x < i ) } by XBOOLE_0:def 4;

then A53: ex x9 being Element of NAT st

( x9 = x & x9 in z & x9 < i ) ;

x in {i} by A52, XBOOLE_0:def 4;

hence contradiction by A53, TARSKI:def 1; :: thesis: verum

then A54: { x where x is Element of NAT : ( x in z & x < i ) } misses {i} by XBOOLE_0:def 7;

A55: y = ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)}) \ {i} by A43, A40, TARSKI:2

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \ {i}) \/ ({(i + 1)} \ {i}) by XBOOLE_1:42

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \ {i}) \/ {(i + 1)} by A16, XBOOLE_1:83

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \ {i}) \/ ( { x where x is Element of NAT : ( x in z & i + 1 < x ) } \ {i})) \/ {(i + 1)} by XBOOLE_1:42

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) \ {i}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by A51, XBOOLE_1:83

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \ {i}) \/ ({i} \ {i})) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by XBOOLE_1:42

.= ((( { x where x is Element of NAT : ( x in z & x < i ) } \ {i}) \/ {}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by XBOOLE_1:37

.= (( { x where x is Element of NAT : ( x in z & x < i ) } \/ {}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) \/ {(i + 1)} by A54, XBOOLE_1:83

.= ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)}) \/ { x where x is Element of NAT : ( x in z & i + 1 < x ) } by XBOOLE_1:4 ;

then {(i + 1)} c= y by XBOOLE_1:7, XBOOLE_1:11;

then A56: {(i + 1)} c= Seg (k + 1) by A18;

{ x where x is Element of NAT : ( x in z & i + 1 < x ) } c= y by A55, XBOOLE_1:7;

then A57: { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= Seg (k + 1) by A18;

now :: thesis: not i in y

hence
not i in y
; :: thesis: s2 = s1 * (Sgm y)assume
i in y
; :: thesis: contradiction

then not i in {i} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not i in {i} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

A58: now :: thesis: for m, n being Nat st m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} & n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } holds

m < n

m < n

let m, n be Nat; :: thesis: ( m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} & n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies m < n )

assume m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} ; :: thesis: ( n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies m < n )

then ( m in { x where x is Element of NAT : ( x in z & x < i ) } or m in {i} ) by XBOOLE_0:def 3;

then A59: ex x9 being Element of NAT st

( ( m = x9 & x9 in z & x9 < i ) or m in {i} ) ;

assume n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ; :: thesis: m < n

then A60: ex x99 being Element of NAT st

( n = x99 & x99 in z & i + 1 < x99 ) ;

0 + i < 1 + i by XREAL_1:6;

then m < i + 1 by A59, TARSKI:def 1, XXREAL_0:2;

hence m < n by A60, XXREAL_0:2; :: thesis: verum

end;assume m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} ; :: thesis: ( n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies m < n )

then ( m in { x where x is Element of NAT : ( x in z & x < i ) } or m in {i} ) by XBOOLE_0:def 3;

then A59: ex x9 being Element of NAT st

( ( m = x9 & x9 in z & x9 < i ) or m in {i} ) ;

assume n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ; :: thesis: m < n

then A60: ex x99 being Element of NAT st

( n = x99 & x99 in z & i + 1 < x99 ) ;

0 + i < 1 + i by XREAL_1:6;

then m < i + 1 by A59, TARSKI:def 1, XXREAL_0:2;

hence m < n by A60, XXREAL_0:2; :: thesis: verum

A61: now :: thesis: for m, n being Nat st m in { x where x is Element of NAT : ( x in z & x < i ) } & n in {i} holds

m < n

m < n

let m, n be Nat; :: thesis: ( m in { x where x is Element of NAT : ( x in z & x < i ) } & n in {i} implies m < n )

assume m in { x where x is Element of NAT : ( x in z & x < i ) } ; :: thesis: ( n in {i} implies m < n )

then A62: ex x9 being Element of NAT st

( m = x9 & x9 in z & x9 < i ) ;

assume n in {i} ; :: thesis: m < n

hence m < n by A62, TARSKI:def 1; :: thesis: verum

end;assume m in { x where x is Element of NAT : ( x in z & x < i ) } ; :: thesis: ( n in {i} implies m < n )

then A62: ex x9 being Element of NAT st

( m = x9 & x9 in z & x9 < i ) ;

assume n in {i} ; :: thesis: m < n

hence m < n by A62, TARSKI:def 1; :: thesis: verum

A63: now :: thesis: for m, n being Nat st m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} & n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } holds

m < n

m < n

let m, n be Nat; :: thesis: ( m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} & n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies m < n )

assume m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} ; :: thesis: ( n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies m < n )

then ( m in { x where x is Element of NAT : ( x in z & x < i ) } or m in {(i + 1)} ) by XBOOLE_0:def 3;

then A64: ex x9 being Element of NAT st

( ( m = x9 & x9 in z & x9 < i ) or m in {(i + 1)} ) ;

assume n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ; :: thesis: m < n

then A65: ex x99 being Element of NAT st

( n = x99 & x99 in z & i + 1 < x99 ) ;

0 + i < 1 + i by XREAL_1:6;

then ( m < i + 1 or m = i + 1 ) by A64, TARSKI:def 1, XXREAL_0:2;

hence m < n by A65, XXREAL_0:2; :: thesis: verum

end;assume m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} ; :: thesis: ( n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } implies m < n )

then ( m in { x where x is Element of NAT : ( x in z & x < i ) } or m in {(i + 1)} ) by XBOOLE_0:def 3;

then A64: ex x9 being Element of NAT st

( ( m = x9 & x9 in z & x9 < i ) or m in {(i + 1)} ) ;

assume n in { x where x is Element of NAT : ( x in z & i + 1 < x ) } ; :: thesis: m < n

then A65: ex x99 being Element of NAT st

( n = x99 & x99 in z & i + 1 < x99 ) ;

0 + i < 1 + i by XREAL_1:6;

then ( m < i + 1 or m = i + 1 ) by A64, TARSKI:def 1, XXREAL_0:2;

hence m < n by A65, XXREAL_0:2; :: thesis: verum

A66: now :: thesis: for m, n being Nat st m in { x where x is Element of NAT : ( x in z & x < i ) } & n in {(i + 1)} holds

m < n

{ x where x is Element of NAT : ( x in z & x < i ) } c= y
by A55, XBOOLE_1:7, XBOOLE_1:11;m < n

let m, n be Nat; :: thesis: ( m in { x where x is Element of NAT : ( x in z & x < i ) } & n in {(i + 1)} implies m < n )

A67: 0 + i < 1 + i by XREAL_1:6;

assume m in { x where x is Element of NAT : ( x in z & x < i ) } ; :: thesis: ( n in {(i + 1)} implies m < n )

then A68: ex x9 being Element of NAT st

( m = x9 & x9 in z & x9 < i ) ;

assume n in {(i + 1)} ; :: thesis: m < n

then n = i + 1 by TARSKI:def 1;

hence m < n by A68, A67, XXREAL_0:2; :: thesis: verum

end;A67: 0 + i < 1 + i by XREAL_1:6;

assume m in { x where x is Element of NAT : ( x in z & x < i ) } ; :: thesis: ( n in {(i + 1)} implies m < n )

then A68: ex x9 being Element of NAT st

( m = x9 & x9 in z & x9 < i ) ;

assume n in {(i + 1)} ; :: thesis: m < n

then n = i + 1 by TARSKI:def 1;

hence m < n by A68, A67, XXREAL_0:2; :: thesis: verum

then { x where x is Element of NAT : ( x in z & x < i ) } c= Seg (k + 1) by A18;

then A69: Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)}) = (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ (Sgm {(i + 1)}) by A56, A66, FINSEQ_3:42;

{ x where x is Element of NAT : ( x in z & x < i ) } \/ {i} c= z by A45, XBOOLE_1:7;

then { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} c= Seg (k + 1) by A42;

then A70: Sgm z = (Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i})) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A45, A46, A58, FINSEQ_3:42;

{i} c= z by A45, XBOOLE_1:7, XBOOLE_1:11;

then {i} c= Seg (k + 1) by A42;

then A71: Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {i}) = (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ (Sgm {i}) by A47, A61, FINSEQ_3:42;

then A72: Sgm z = ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A4, A70, FINSEQ_3:44;

{ x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} c= y by A55, XBOOLE_1:7;

then { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} c= Seg (k + 1) by A18;

then A73: Sgm y = (Sgm ( { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)})) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A55, A57, A63, FINSEQ_3:42;

then A74: Sgm y = ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A69, FINSEQ_3:44;

A75: now :: thesis: for x being set st x in dom (Sgm z) holds

( ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) & ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) )

rng (Sgm z) c= dom s1
by A9, A8, FINSEQ_1:def 13;( ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) & ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) )

let x be set ; :: thesis: ( x in dom (Sgm z) implies ( ( (Sgm z) . b_{1} <> i implies (Sgm y) . b_{1} = (Sgm z) . b_{1} ) & ( (Sgm z) . b_{1} = i implies (Sgm y) . b_{1} = i + 1 ) ) )

A76: len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + (len <*i*>) by FINSEQ_1:22

.= (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + 1 by FINSEQ_1:40

.= (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + (len <*(i + 1)*>) by FINSEQ_1:40

.= len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) by FINSEQ_1:22 ;

assume A77: x in dom (Sgm z) ; :: thesis: ( ( (Sgm z) . b_{1} <> i implies (Sgm y) . b_{1} = (Sgm z) . b_{1} ) & ( (Sgm z) . b_{1} = i implies (Sgm y) . b_{1} = i + 1 ) )

then reconsider x9 = x as Element of NAT ;

A78: dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) = Seg (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) by FINSEQ_1:def 3

.= dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) by A76, FINSEQ_1:def 3 ;

end;A76: len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + (len <*i*>) by FINSEQ_1:22

.= (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + 1 by FINSEQ_1:40

.= (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + (len <*(i + 1)*>) by FINSEQ_1:40

.= len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) by FINSEQ_1:22 ;

assume A77: x in dom (Sgm z) ; :: thesis: ( ( (Sgm z) . b

then reconsider x9 = x as Element of NAT ;

A78: dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) = Seg (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) by FINSEQ_1:def 3

.= dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) by A76, FINSEQ_1:def 3 ;

per cases
( x9 in dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) or ex x99 being Nat st

( x99 in dom (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) & x9 = (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) + x99 ) ) by A72, A77, FINSEQ_1:25;

end;

( x99 in dom (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) & x9 = (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) + x99 ) ) by A72, A77, FINSEQ_1:25;

suppose A79:
x9 in dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)
; :: thesis: ( ( (Sgm z) . b_{1} <> i implies (Sgm y) . b_{1} = (Sgm z) . b_{1} ) & ( (Sgm z) . b_{1} = i implies (Sgm y) . b_{1} = i + 1 ) )

end;

per cases
( x9 in dom (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) or ex x99 being Nat st

( x99 in dom <*i*> & x9 = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + x99 ) ) by A79, FINSEQ_1:25;

end;

( x99 in dom <*i*> & x9 = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + x99 ) ) by A79, FINSEQ_1:25;

suppose A80:
x9 in dom (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )
; :: thesis: ( ( (Sgm z) . b_{1} <> i implies (Sgm y) . b_{1} = (Sgm z) . b_{1} ) & ( (Sgm z) . b_{1} = i implies (Sgm y) . b_{1} = i + 1 ) )

then A81: (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) . x9 =
((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) . x9
by FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A79, FINSEQ_1:def 7

.= (Sgm z) . x9 by A4, A70, A71, FINSEQ_3:44 ;

(Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) . x9 = ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) . x9 by A80, FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A78, A79, FINSEQ_1:def 7

.= (Sgm y) . x9 by A73, A69, FINSEQ_3:44 ;

hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) by A81; :: thesis: ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 )

thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis: verum

end;.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A79, FINSEQ_1:def 7

.= (Sgm z) . x9 by A4, A70, A71, FINSEQ_3:44 ;

(Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) . x9 = ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) . x9 by A80, FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A78, A79, FINSEQ_1:def 7

.= (Sgm y) . x9 by A73, A69, FINSEQ_3:44 ;

hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) by A81; :: thesis: ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 )

thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis: verum

proof

assume
(Sgm z) . x = i
; :: thesis: (Sgm y) . x = i + 1

then i in rng (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) by A80, A81, FUNCT_1:3;

then i in { x where x is Element of NAT : ( x in z & x < i ) } by A47, FINSEQ_1:def 13;

then ex x999 being Element of NAT st

( x999 = i & x999 in z & x999 < i ) ;

hence (Sgm y) . x = i + 1 ; :: thesis: verum

end;then i in rng (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) by A80, A81, FUNCT_1:3;

then i in { x where x is Element of NAT : ( x in z & x < i ) } by A47, FINSEQ_1:def 13;

then ex x999 being Element of NAT st

( x999 = i & x999 in z & x999 < i ) ;

hence (Sgm y) . x = i + 1 ; :: thesis: verum

suppose
ex x99 being Nat st

( x99 in dom <*i*> & x9 = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + x99 ) ; :: thesis: ( ( (Sgm z) . b_{1} <> i implies (Sgm y) . b_{1} = (Sgm z) . b_{1} ) & ( (Sgm z) . b_{1} = i implies (Sgm y) . b_{1} = i + 1 ) )

( x99 in dom <*i*> & x9 = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + x99 ) ; :: thesis: ( ( (Sgm z) . b

then consider x99 being Nat such that

A82: x99 in dom <*i*> and

A83: x9 = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + x99 ;

A84: x99 in Seg 1 by A82, FINSEQ_1:38;

then A85: x99 = 1 by FINSEQ_1:2, TARSKI:def 1;

then i = <*i*> . x99 by FINSEQ_1:40

.= ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) . x9 by A82, A83, FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A79, FINSEQ_1:def 7

.= (Sgm z) . x9 by A4, A70, A71, FINSEQ_3:44 ;

hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) ; :: thesis: ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 )

thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis: verum

end;A82: x99 in dom <*i*> and

A83: x9 = (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + x99 ;

A84: x99 in Seg 1 by A82, FINSEQ_1:38;

then A85: x99 = 1 by FINSEQ_1:2, TARSKI:def 1;

then i = <*i*> . x99 by FINSEQ_1:40

.= ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) . x9 by A82, A83, FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A79, FINSEQ_1:def 7

.= (Sgm z) . x9 by A4, A70, A71, FINSEQ_3:44 ;

hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) ; :: thesis: ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 )

thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis: verum

proof

assume
(Sgm z) . x = i
; :: thesis: (Sgm y) . x = i + 1

A86: x99 in dom <*(i + 1)*> by A84, FINSEQ_1:38;

i + 1 = <*(i + 1)*> . x99 by A85, FINSEQ_1:40

.= ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) . x9 by A83, A86, FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A78, A79, FINSEQ_1:def 7 ;

hence (Sgm y) . x = i + 1 by A73, A69, FINSEQ_3:44; :: thesis: verum

end;A86: x99 in dom <*(i + 1)*> by A84, FINSEQ_1:38;

i + 1 = <*(i + 1)*> . x99 by A85, FINSEQ_1:40

.= ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) . x9 by A83, A86, FINSEQ_1:def 7

.= (((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } )) . x9 by A78, A79, FINSEQ_1:def 7 ;

hence (Sgm y) . x = i + 1 by A73, A69, FINSEQ_3:44; :: thesis: verum

suppose
ex x99 being Nat st

( x99 in dom (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) & x9 = (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) + x99 ) ; :: thesis: ( ( (Sgm z) . b_{1} <> i implies (Sgm y) . b_{1} = (Sgm z) . b_{1} ) & ( (Sgm z) . b_{1} = i implies (Sgm y) . b_{1} = i + 1 ) )

( x99 in dom (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) & x9 = (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) + x99 ) ; :: thesis: ( ( (Sgm z) . b

then consider x99 being Nat such that

A87: x99 in dom (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) and

A88: x9 = (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) + x99 ;

(Sgm y) . x9 = (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) . x99 by A74, A76, A87, A88, FINSEQ_1:def 7;

hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) by A72, A87, A88, FINSEQ_1:def 7; :: thesis: ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 )

thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis: verum

end;A87: x99 in dom (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) and

A88: x9 = (len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>)) + x99 ;

(Sgm y) . x9 = (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) . x99 by A74, A76, A87, A88, FINSEQ_1:def 7;

hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) by A72, A87, A88, FINSEQ_1:def 7; :: thesis: ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 )

thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis: verum

proof

assume
(Sgm z) . x = i
; :: thesis: (Sgm y) . x = i + 1

then (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) . x99 = i by A72, A87, A88, FINSEQ_1:def 7;

then i in rng (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A87, FUNCT_1:3;

then i in { x where x is Element of NAT : ( x in z & i + 1 < x ) } by A57, FINSEQ_1:def 13;

then ex x999 being Element of NAT st

( x999 = i & x999 in z & i + 1 < x999 ) ;

then (i + 1) - i < i - i by XREAL_1:9;

then 1 < 0 ;

hence (Sgm y) . x = i + 1 ; :: thesis: verum

end;then (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) . x99 = i by A72, A87, A88, FINSEQ_1:def 7;

then i in rng (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A87, FUNCT_1:3;

then i in { x where x is Element of NAT : ( x in z & i + 1 < x ) } by A57, FINSEQ_1:def 13;

then ex x999 being Element of NAT st

( x999 = i & x999 in z & i + 1 < x999 ) ;

then (i + 1) - i < i - i by XREAL_1:9;

then 1 < 0 ;

hence (Sgm y) . x = i + 1 ; :: thesis: verum

then A89: dom (s1 * (Sgm z)) = dom (Sgm z) by RELAT_1:27;

then A90: dom (s1 * (Sgm y)) = dom (s1 * (Sgm z)) by A39, A19, RELAT_1:27;

now :: thesis: for x being object st x in dom (s1 * (Sgm y)) holds

(s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x

hence
s2 = s1 * (Sgm y)
by A10, A39, A19, A89, FUNCT_1:2, RELAT_1:27; :: thesis: verum(s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x

let x be object ; :: thesis: ( x in dom (s1 * (Sgm y)) implies (s1 * (Sgm y)) . b_{1} = (s1 * (Sgm z)) . b_{1} )

assume A91: x in dom (s1 * (Sgm y)) ; :: thesis: (s1 * (Sgm y)) . b_{1} = (s1 * (Sgm z)) . b_{1}

then A92: x in dom (Sgm z) by A39, A19, RELAT_1:27;

A93: x in dom (s1 * (Sgm z)) by A39, A19, A89, A91, RELAT_1:27;

end;assume A91: x in dom (s1 * (Sgm y)) ; :: thesis: (s1 * (Sgm y)) . b

then A92: x in dom (Sgm z) by A39, A19, RELAT_1:27;

A93: x in dom (s1 * (Sgm z)) by A39, A19, A89, A91, RELAT_1:27;

per cases
( (Sgm z) . x = i or (Sgm z) . x <> i )
;

end;

suppose A94:
(Sgm z) . x = i
; :: thesis: (s1 * (Sgm y)) . b_{1} = (s1 * (Sgm z)) . b_{1}

(s1 * (Sgm y)) . x =
s1 . ((Sgm y) . x)
by A91, FUNCT_1:12

.= s1 . ((Sgm z) . x) by A5, A75, A92, A94

.= (s1 * (Sgm z)) . x by A90, A91, FUNCT_1:12 ;

hence (s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x ; :: thesis: verum

end;.= s1 . ((Sgm z) . x) by A5, A75, A92, A94

.= (s1 * (Sgm z)) . x by A90, A91, FUNCT_1:12 ;

hence (s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x ; :: thesis: verum

A96: y c= Seg (k + 1) and

A97: not i in y and

A98: s2 = s1 * (Sgm y) ;

now :: thesis: ex x being set st

( x c= dom s19 & s2 = s19 * (Sgm x) )

hence
s19 is_finer_than s2
; :: thesis: verum( x c= dom s19 & s2 = s19 * (Sgm x) )

consider x being set such that

A99: Sgm x = ((Sgm ((Seg (k + 1)) \ {i})) ") * (Sgm y) and

A100: x c= Seg k by A3, A96, A97, Lm38;

take x = x; :: thesis: ( x c= dom s19 & s2 = s19 * (Sgm x) )

ex m being Nat st

( len s1 = m + 1 & len (Del (s1,i)) = m ) by A1, FINSEQ_3:104;

hence x c= dom s19 by A6, A100, FINSEQ_1:def 3; :: thesis: s2 = s19 * (Sgm x)

set f = Sgm ((Seg (k + 1)) \ {i});

set X = dom (Sgm ((Seg (k + 1)) \ {i}));

set Y = rng (Sgm ((Seg (k + 1)) \ {i}));

reconsider f = Sgm ((Seg (k + 1)) \ {i}) as Function of (dom (Sgm ((Seg (k + 1)) \ {i}))),(rng (Sgm ((Seg (k + 1)) \ {i}))) by FUNCT_2:1;

A101: f is one-to-one by FINSEQ_3:92, XBOOLE_1:36;

(Seg (k + 1)) \ {i} c= Seg (k + 1) by XBOOLE_1:36;

then A102: rng f = (Seg (k + 1)) \ {i} by FINSEQ_1:def 13;

then A104: rng (Sgm y) c= rng f by A96, FINSEQ_1:def 13;

.= ((s1 * f) * (f ")) * (Sgm y) by A99, RELAT_1:36

.= (s1 * (f * (f "))) * (Sgm y) by RELAT_1:36

.= (s1 * (id (rng f))) * (Sgm y) by A101, A105, FUNCT_2:29

.= s1 * ((id (rng f)) * (Sgm y)) by RELAT_1:36

.= s1 * (Sgm y) by A104, RELAT_1:53 ;

hence s2 = s19 * (Sgm x) by A98; :: thesis: verum

end;A99: Sgm x = ((Sgm ((Seg (k + 1)) \ {i})) ") * (Sgm y) and

A100: x c= Seg k by A3, A96, A97, Lm38;

take x = x; :: thesis: ( x c= dom s19 & s2 = s19 * (Sgm x) )

ex m being Nat st

( len s1 = m + 1 & len (Del (s1,i)) = m ) by A1, FINSEQ_3:104;

hence x c= dom s19 by A6, A100, FINSEQ_1:def 3; :: thesis: s2 = s19 * (Sgm x)

set f = Sgm ((Seg (k + 1)) \ {i});

set X = dom (Sgm ((Seg (k + 1)) \ {i}));

set Y = rng (Sgm ((Seg (k + 1)) \ {i}));

reconsider f = Sgm ((Seg (k + 1)) \ {i}) as Function of (dom (Sgm ((Seg (k + 1)) \ {i}))),(rng (Sgm ((Seg (k + 1)) \ {i}))) by FUNCT_2:1;

A101: f is one-to-one by FINSEQ_3:92, XBOOLE_1:36;

(Seg (k + 1)) \ {i} c= Seg (k + 1) by XBOOLE_1:36;

then A102: rng f = (Seg (k + 1)) \ {i} by FINSEQ_1:def 13;

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

x9 in rng f

then
y c= rng f
;x9 in rng f

let x9 be object ; :: thesis: ( x9 in y implies x9 in rng f )

assume A103: x9 in y ; :: thesis: x9 in rng f

then not x9 in {i} by A97, TARSKI:def 1;

hence x9 in rng f by A96, A102, A103, XBOOLE_0:def 5; :: thesis: verum

end;assume A103: x9 in y ; :: thesis: x9 in rng f

then not x9 in {i} by A97, TARSKI:def 1;

hence x9 in rng f by A96, A102, A103, XBOOLE_0:def 5; :: thesis: verum

then A104: rng (Sgm y) c= rng f by A96, FINSEQ_1:def 13;

A105: now :: thesis: not rng f = {}

s19 * (Sgm x) =
(s1 * f) * (Sgm x)
by A6, FINSEQ_1:def 3
1 <= i
by A3, FINSEQ_1:1;

then A106: 1 + 1 <= i + 1 by XREAL_1:6;

i + 1 <= len s1 by A11, FINSEQ_1:1;

then 2 <= len s1 by A106, XXREAL_0:2;

then Seg 2 c= Seg (k + 1) by FINSEQ_1:5;

then A107: (Seg 2) \ {i} c= rng f by A102, XBOOLE_1:33;

assume A108: rng f = {} ; :: thesis: contradiction

end;then A106: 1 + 1 <= i + 1 by XREAL_1:6;

i + 1 <= len s1 by A11, FINSEQ_1:1;

then 2 <= len s1 by A106, XXREAL_0:2;

then Seg 2 c= Seg (k + 1) by FINSEQ_1:5;

then A107: (Seg 2) \ {i} c= rng f by A102, XBOOLE_1:33;

assume A108: rng f = {} ; :: thesis: contradiction

.= ((s1 * f) * (f ")) * (Sgm y) by A99, RELAT_1:36

.= (s1 * (f * (f "))) * (Sgm y) by RELAT_1:36

.= (s1 * (id (rng f))) * (Sgm y) by A101, A105, FUNCT_2:29

.= s1 * ((id (rng f)) * (Sgm y)) by RELAT_1:36

.= s1 * (Sgm y) by A104, RELAT_1:53 ;

hence s2 = s19 * (Sgm x) by A98; :: thesis: verum