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 ;
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 ;
then 1 <= len s1 by ;
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 ;
now :: thesis: ex y being set st
( y c= Seg (k + 1) & not i in y & s2 = s1 * (Sgm y) )
per cases ( not i in z or i in z ) ;
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) )

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 ; :: 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;
suppose A13: i in z ; :: thesis: ex y being set st
( 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}end;
then {(i + 1)} /\ {i} = {} by XBOOLE_0:def 1;
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 ;
then A17: z \/ {(i + 1)} c= Seg (k + 1) by ;
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 ;
reconsider y9 = y, z = z as finite set by A9;
A20: dom (Sgm y9) = Seg (card y9) by ;
i in z \/ {(i + 1)} by ;
then {i} c= z \/ {(i + 1)} by ZFMISC_1:31;
then card ((z \/ {(i + 1)}) \ {i}) = (card (z \/ {(i + 1)})) - () 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
A23: 0 + i < 1 + i by XREAL_1:6;
assume i + 1 in z ; :: thesis: contradiction
then i + 1 in rng (Sgm z) by ;
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 ;
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 ;
A28: dom (Sgm z) = Seg (len (Sgm z)) by FINSEQ_1:def 3;
then A29: x9 <= len (Sgm z) by ;
1 <= x99 by ;
then x9 < x99 by ;
then reconsider l = x99 - x9 as Element of NAT by INT_1:5;
per cases ( l = 0 or 0 < l ) ;
suppose A30: 0 < l ; :: thesis: contradiction
set x999 = x9 + 1;
0 + 1 < l + 1 by ;
then (x9 + 1) - x9 <= x99 - x9 by NAT_1:13;
then A31: x9 + 1 <= x99 by XREAL_1:9;
x99 <= len (Sgm z) by ;
then A32: x9 + 1 <= len (Sgm z) by ;
A33: ( 1 + x9 > 0 + x9 & 1 <= x9 ) by ;
then 1 <= x9 + 1 by XXREAL_0:2;
then x9 + 1 in dom (Sgm z) by ;
then reconsider k3 = (Sgm z) . (x9 + 1) as Element of NAT by FINSEQ_2:11;
i < k3 by ;
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 ;
then A36: x9 + 1 in dom s2 by ;
A37: s2 is strictly_decreasing by A7;
A38: x9 in dom s2 by ;
then reconsider H1 = s2 . x9, H2 = s2 . (x9 + 1) as Element of the_stable_subgroups_of G by ;
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 ;
s2 . x9 = s1 . ((Sgm z) . x9) by
.= s2 . (x9 + 1) by ;
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;
end;
end;
then card (z \/ {(i + 1)}) = (card z) + 1 by CARD_2:41;
then A39: dom (Sgm y9) = dom (Sgm z) by ;
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
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 b1 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: b1 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 ) ) ;
per cases ( ( x = x9 & x9 in z & x9 < i ) or x in {i} or ( x = x99 & x99 in z & i + 1 < x99 ) ) by A41;
suppose ( x = x9 & x9 in z & x9 < i ) ; :: thesis: b1 in z
hence x in z ; :: thesis: verum
end;
suppose x in {i} ; :: thesis: b1 in z
hence x in z by ; :: thesis: verum
end;
suppose ( x = x99 & x99 in z & i + 1 < x99 ) ; :: thesis: b1 in z
hence x in z ; :: thesis: verum
end;
end;
end;
A42: z c= Seg (k + 1) by ;
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 ) }
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 ;
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 ;
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;
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 ;
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 ;
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}
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 ;
then x9 = i by ;
then (i + 1) - i < i - i by ;
then 1 < 0 ;
hence contradiction ; :: thesis: verum
end;
then { x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i} = {} by XBOOLE_0:def 1;
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}
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 ;
hence contradiction by A53, TARSKI:def 1; :: thesis: verum
end;
then { x where x is Element of NAT : ( x in z & x < i ) } /\ {i} = {} by XBOOLE_0:def 1;
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
.= ((( { 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
.= ((( { 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
.= ((( { 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
.= ( { 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 ;
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 ;
then A57: { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= Seg (k + 1) by A18;
hence not i in y ; :: thesis: s2 = s1 * (Sgm y)
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
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 ;
hence m < n by ; :: thesis: verum
end;
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
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 ; :: thesis: verum
end;
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
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 ;
hence m < n by ; :: thesis: verum
end;
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
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 ; :: thesis: verum
end;
{ x where x is Element of NAT : ( x in z & x < i ) } c= y by ;
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 ;
{ x where x is Element of NAT : ( x in z & x < i ) } \/ {i} c= z by ;
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 ;
{i} c= z by ;
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 ) } ) ^ () by ;
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 ;
{ x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} c= y by ;
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 ;
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 ;
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 ) )
let x be set ; :: thesis: ( x in dom (Sgm z) implies ( ( (Sgm z) . b1 <> i implies (Sgm y) . b1 = (Sgm z) . b1 ) & ( (Sgm z) . b1 = i implies (Sgm y) . b1 = 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 ) } )) + () 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) . b1 <> i implies (Sgm y) . b1 = (Sgm z) . b1 ) & ( (Sgm z) . b1 = i implies (Sgm y) . b1 = 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 ;
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 ;
suppose A79: x9 in dom ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) ; :: thesis: ( ( (Sgm z) . b1 <> i implies (Sgm y) . b1 = (Sgm z) . b1 ) & ( (Sgm z) . b1 = i implies (Sgm y) . b1 = i + 1 ) )
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 ;
suppose A80: x9 in dom (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ; :: thesis: ( ( (Sgm z) . b1 <> i implies (Sgm y) . b1 = (Sgm z) . b1 ) & ( (Sgm z) . b1 = i implies (Sgm y) . b1 = 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
.= (Sgm z) . x9 by ;
(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
.= (((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
.= (Sgm y) . x9 by ;
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 ;
then i in { x where x is Element of NAT : ( x in z & x < i ) } by ;
then ex x999 being Element of NAT st
( x999 = i & x999 in z & x999 < i ) ;
hence (Sgm y) . x = i + 1 ; :: thesis: verum
end;
end;
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) . b1 <> i implies (Sgm y) . b1 = (Sgm z) . b1 ) & ( (Sgm z) . b1 = i implies (Sgm y) . b1 = i + 1 ) )
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 ;
then A85: x99 = 1 by ;
then i = <*i*> . x99 by FINSEQ_1:40
.= ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*i*>) . x9 by
.= (((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
.= (Sgm z) . x9 by ;
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 ;
i + 1 = <*(i + 1)*> . x99 by
.= ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) . x9 by
.= (((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 ;
hence (Sgm y) . x = i + 1 by ; :: thesis: verum
end;
end;
end;
end;
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) . b1 <> i implies (Sgm y) . b1 = (Sgm z) . b1 ) & ( (Sgm z) . b1 = i implies (Sgm y) . b1 = i + 1 ) )
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 ;
hence ( (Sgm z) . x <> i implies (Sgm y) . x = (Sgm z) . x ) by ; :: 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 ;
then i in rng (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by ;
then i in { x where x is Element of NAT : ( x in z & i + 1 < x ) } by ;
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;
end;
end;
end;
rng (Sgm z) c= dom s1 by ;
then A89: dom (s1 * (Sgm z)) = dom (Sgm z) by RELAT_1:27;
then A90: dom (s1 * (Sgm y)) = dom (s1 * (Sgm z)) by ;
now :: thesis: for x being object st x in dom (s1 * (Sgm y)) holds
(s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x
let x be object ; :: thesis: ( x in dom (s1 * (Sgm y)) implies (s1 * (Sgm y)) . b1 = (s1 * (Sgm z)) . b1 )
assume A91: x in dom (s1 * (Sgm y)) ; :: thesis: (s1 * (Sgm y)) . b1 = (s1 * (Sgm z)) . b1
then A92: x in dom (Sgm z) by ;
A93: x in dom (s1 * (Sgm z)) by ;
per cases ) . x = i or (Sgm z) . x <> i ) ;
suppose A94: (Sgm z) . x = i ; :: thesis: (s1 * (Sgm y)) . b1 = (s1 * (Sgm z)) . b1
(s1 * (Sgm y)) . x = s1 . ((Sgm y) . x) by
.= s1 . ((Sgm z) . x) by A5, A75, A92, A94
.= (s1 * (Sgm z)) . x by ;
hence (s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x ; :: thesis: verum
end;
suppose A95: (Sgm z) . x <> i ; :: thesis: (s1 * (Sgm y)) . b1 = (s1 * (Sgm z)) . b1
(s1 * (Sgm y)) . x = s1 . ((Sgm y) . x) by
.= s1 . ((Sgm z) . x) by
.= (s1 * (Sgm z)) . x by ;
hence (s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x ; :: thesis: verum
end;
end;
end;
hence s2 = s1 * (Sgm y) by ; :: thesis: verum
end;
end;
end;
then consider y being set such that
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) )
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 ;
hence x c= dom s19 by ; :: 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 ;
(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
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 ;
hence x9 in rng f by ; :: thesis: verum
end;
then y c= rng f ;
then A104: rng (Sgm y) c= rng f by ;
A105: now :: thesis: not rng f = {}
1 <= i by ;
then A106: 1 + 1 <= i + 1 by XREAL_1:6;
i + 1 <= len s1 by ;
then 2 <= len s1 by ;
then Seg 2 c= Seg (k + 1) by FINSEQ_1:5;
then A107: (Seg 2) \ {i} c= rng f by ;
assume A108: rng f = {} ; :: thesis: contradiction
end;
s19 * (Sgm x) = (s1 * f) * (Sgm x) by
.= ((s1 * f) * (f ")) * (Sgm y) by
.= (s1 * (f * (f "))) * (Sgm y) by RELAT_1:36
.= (s1 * (id (rng f))) * (Sgm y) by
.= s1 * ((id (rng f)) * (Sgm y)) by RELAT_1:36
.= s1 * (Sgm y) by ;
hence s2 = s19 * (Sgm x) by A98; :: thesis: verum
end;
hence s19 is_finer_than s2 ; :: thesis: verum