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:3;
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 number ;
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:3;
then 1 <= len s1 by A4, XXREAL_0:2;
then 1 - 1 <= (len s1) - 1 by XREAL_1:11;
then reconsider k = k as Element of NAT by INT_1:16;
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) by Def32;
A11: i + 1 in Seg (len s1) by A2, FINSEQ_1:def 3;
now
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 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;
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 {(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 A11, ZFMISC_1:37;
then A17: z \/ {(i + 1)} c= Seg (k + 1) by A9, A8, XBOOLE_1:8;
hence A18: y c= Seg (k + 1) by XBOOLE_1: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:45, XBOOLE_1:1;
i in z \/ {(i + 1)} by A13, XBOOLE_0:def 3;
then {i} c= z \/ {(i + 1)} by ZFMISC_1:37;
then card ((z \/ {(i + 1)}) \ {i}) = (card (z \/ {(i + 1)})) - (card {i}) by CARD_2:63;
then A21: card y9 = (card (z \/ {(i + 1)})) - 1 by CARD_1:50;
A22: now
A23: 0 + i < 1 + i by XREAL_1:8;
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 set such that
A24: x99 in dom (Sgm z) and
A25: i + 1 = (Sgm z) . x99 by FUNCT_1:def 5;
i in rng (Sgm z) by A9, A8, A13, FINSEQ_1:def 13;
then consider x9 being set such that
A26: x9 in dom (Sgm z) and
A27: i = (Sgm z) . x9 by FUNCT_1:def 5;
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:3;
1 <= x99 by A24, A28, FINSEQ_1:3;
then x9 < x99 by A9, A8, A27, A25, A23, A29, FINSEQ_3:46;
then reconsider l = x99 - x9 as Element of NAT by INT_1:18;
per cases ( l = 0 or 0 < l ) ;
suppose A30: 0 < l ; :: thesis: contradiction
set x999 = x9 + 1;
0 + 1 < l + 1 by A30, XREAL_1:8;
then (x9 + 1) - x9 <= x99 - x9 by NAT_1:13;
then A31: x9 + 1 <= x99 by XREAL_1:11;
x99 <= len (Sgm z) by A24, A28, FINSEQ_1:3;
then A32: x9 + 1 <= len (Sgm z) by A31, XXREAL_0:2;
A33: ( 1 + x9 > 0 + x9 & 1 <= x9 ) by A26, A28, FINSEQ_1:3, XREAL_1:8;
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:13;
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:3, 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:21;
A37: s2 is strictly_decreasing by A7, Def34;
A38: x9 in dom s2 by A1, A10, A26, A27, FUNCT_1:21;
then reconsider H1 = s2 . x9, H2 = s2 . (x9 + 1) as Element of the_stable_subgroups_of G by A36, FINSEQ_2:13;
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, Def31;
s2 . x9 = s1 . ((Sgm z) . x9) by A10, A26, FUNCT_1:23
.= s2 . (x9 + 1) by A5, A9, A10, A8, A27, A24, A25, A35, A34, FINSEQ_1:def 13, FUNCT_1:23 ;
then the carrier of H1 = the carrier of H2 ;
then H1 ./. H2 is trivial by Th77;
hence contradiction by A38, A36, A37, Def33; :: thesis: verum
end;
end;
end;
then card (z \/ {(i + 1)}) = (card z) + 1 by CARD_2:54;
then A39: dom (Sgm y9) = dom (Sgm z) by A9, A8, A21, A20, FINSEQ_3:45;
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
let x be set ; :: 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 = 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 A9, FINSEQ_1:def 3;
A43: now
let x be set ; :: 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;
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;
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, XBOOLE_1:1;
{ 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, XBOOLE_1:1;
now
let x be set ; :: 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:11;
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
let x be set ; :: 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;
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 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, XBOOLE_1:1;
{ 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, XBOOLE_1:1;
hence not i in y ; :: thesis: s2 = s1 * (Sgm y)
A58: now
let m, n be Element of 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:8;
then m < i + 1 by A59, TARSKI:def 1, XXREAL_0:2;
hence m < n by A60, XXREAL_0:2; :: thesis: verum
end;
A61: now
let m, n be Element of 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;
A63: now
let m, n be Element of 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:8;
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;
A66: now
let m, n be Element of 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:8;
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;
{ x where x is Element of NAT : ( x in z & x < i ) } c= y by A55, XBOOLE_1:7, XBOOLE_1:11;
then { x where x is Element of NAT : ( x in z & x < i ) } c= Seg (k + 1) by A18, XBOOLE_1:1;
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:48;
{ 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, XBOOLE_1:1;
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:48;
{i} c= z by A45, XBOOLE_1:7, XBOOLE_1:11;
then {i} c= Seg (k + 1) by A42, XBOOLE_1:1;
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:48;
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:50;
{ 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, XBOOLE_1:1;
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:48;
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:50;
A75: now
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 ) } )) + (len <*i*>) by FINSEQ_1:35
.= (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + 1 by FINSEQ_1:57
.= (len (Sgm { x where x is Element of NAT : ( x in z & x < i ) } )) + (len <*(i + 1)*>) by FINSEQ_1:57
.= len ((Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ^ <*(i + 1)*>) by FINSEQ_1:35 ;
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 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:38;
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 A79, FINSEQ_1:38;
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 A79, FINSEQ_1:def 7
.= (Sgm z) . x9 by A4, A70, A71, FINSEQ_3:50 ;
(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:50 ;
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:12;
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;
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 A82, FINSEQ_1:55;
then A85: x99 = 1 by FINSEQ_1:4, TARSKI:def 1;
then i = <*i*> . x99 by FINSEQ_1:57
.= ((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:50 ;
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:55;
i + 1 = <*(i + 1)*> . x99 by A85, FINSEQ_1:57
.= ((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:50; :: 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 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:12;
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:11;
then 1 < 0 ;
hence (Sgm y) . x = i + 1 ; :: thesis: verum
end;
end;
end;
end;
rng (Sgm z) c= dom s1 by A9, A8, FINSEQ_1:def 13;
then A89: dom (s1 * (Sgm z)) = dom (Sgm z) by RELAT_1:46;
then A90: dom (s1 * (Sgm y)) = dom (s1 * (Sgm z)) by A39, A19, RELAT_1:46;
now
let x be set ; :: 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 A39, A19, RELAT_1:46;
A93: x in dom (s1 * (Sgm z)) by A39, A19, A89, A91, RELAT_1:46;
per cases ( (Sgm z) . 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 A91, FUNCT_1:22
.= s1 . ((Sgm z) . x) by A5, A75, A92, A94
.= (s1 * (Sgm z)) . x by A90, A91, FUNCT_1:22 ;
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 A91, FUNCT_1:22
.= s1 . ((Sgm z) . x) by A75, A92, A95
.= (s1 * (Sgm z)) . x by A93, FUNCT_1:22 ;
hence (s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x ; :: thesis: verum
end;
end;
end;
hence s2 = s1 * (Sgm y) by A10, A39, A19, A89, FUNCT_1:9, RELAT_1:46; :: 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
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, Lm39;
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:113;
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:3;
A101: f is one-to-one by FINSEQ_3:99, 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
let x9 be set ; :: 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;
then y c= rng f by TARSKI:def 3;
then A104: rng (Sgm y) c= rng f by A96, FINSEQ_1:def 13;
A105: now
1 <= i by A3, FINSEQ_1:3;
then A106: 1 + 1 <= i + 1 by XREAL_1:8;
i + 1 <= len s1 by A11, FINSEQ_1:3;
then 2 <= len s1 by A106, XXREAL_0:2;
then Seg 2 c= Seg (k + 1) by FINSEQ_1:7;
then A107: (Seg 2) \ {i} c= rng f by A102, XBOOLE_1:33;
assume A108: rng f = {} ; :: thesis: contradiction
end;
s19 * (Sgm x) = (s1 * f) * (Sgm x) by A6, FINSEQ_1:def 3
.= ((s1 * f) * (f ")) * (Sgm y) by A99, RELAT_1:55
.= (s1 * (f * (f "))) * (Sgm y) by RELAT_1:55
.= (s1 * (id (rng f))) * (Sgm y) by A101, A105, FUNCT_2:35
.= s1 * ((id (rng f)) * (Sgm y)) by RELAT_1:55
.= s1 * (Sgm y) by A104, RELAT_1:79 ;
hence s2 = s19 * (Sgm x) by A98; :: thesis: verum
end;
hence s19 is_finer_than s2 by Def32; :: thesis: verum