let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let s1, s19, s2 be CompositionSeries of G; :: thesis:
let i be Nat; :: thesis:
assume that
A1: i in dom s1 and
A2: i + 1 in dom s1 ; :: thesis:
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:
reconsider k = (len s1) - 1 as Integer ;
assume A6: s19 = Del (s1,i) ; :: thesis:
assume A7: s2 is jordan_holder ; :: thesis:
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:
then consider z being set such that
A9: z c= dom s1 and
A10: s2 = s1 * (Sgm z) ;
a9: z is included_in_Seg by A8, A9;
A11: i + 1 in Seg (len s1) by A2, FINSEQ_1:def 3;

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

end;

suppose A13: i in z ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A14: x in {(i + 1)} /\ {i} ; :: thesis:
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:

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:
{(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;
then a17: z \/ {(i + 1)} is included_in_Seg ;
thus A18: y c= Seg (k + 1) by A17; :: thesis:
then a18: y is included_in_Seg ;
y c= dom s1 by A18, FINSEQ_1:def 3;
then A19: rng (Sgm y) c= dom s1 by a18, FINSEQ_1:def 14;
reconsider y9 = y, z = z as finite set by A9;
A20: dom (Sgm y9) = Seg (card y9) by a17, FINSEQ_3:40;
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:

A23: 0 + i < 1 + i by XREAL_1:6;
assume i + 1 in z ; :: thesis:
then i + 1 in rng (Sgm z) by a9, FINSEQ_1:def 14;
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, A13, FINSEQ_1:def 14;
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, A27, A25, A23, A29, FINSEQ_3:41;
then reconsider l = x99 - x9 as Element of NAT by INT_1:5;

per cases ;

suppose l = 0 ; :: thesis:

hence contradiction by A27, A25, A23; :: thesis:

end;

suppose A30: 0 < l ; :: thesis:

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, A27, A33, A32, FINSEQ_1:def 14;
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 a9, A2, A10, A24, A25, A34, FINSEQ_1:def 14, 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 a9, A5, A10, A27, A24, A25, A35, A34, FINSEQ_1:def 14, 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:

end;

then card (z \/ {(i + 1)}) = (card z) + 1 by CARD_2:41;
then A39: dom (Sgm y9) = dom (Sgm z) by a9, 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:

let x be object ; :: thesis:
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:
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 by A41;

suppose ( x = x9 & x9 in z & x9 < i ) ; :: thesis:

hence x in z ; :: thesis:

end;

suppose x in {i} ; :: thesis:

hence x in z by A13, TARSKI:def 1; :: thesis:

end;

suppose ( x = x99 & x99 in z & i + 1 < x99 ) ; :: thesis:

hence x in z ; :: thesis:

end;

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

A43: now :: thesis:

let x be object ; :: thesis:
assume A44: x in z ; :: thesis:
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:

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 { x where x is Element of NAT : ( x in z & i + 1 < x ) } c= Seg (k + 1) by A42;
then a46: { x where x is Element of NAT : ( x in z & i + 1 < x ) } is included_in_Seg ;

now :: thesis:

let x be object ; :: thesis:
assume A48: x in { x where x is Element of NAT : ( x in z & i + 1 < x ) } /\ {i} ; :: thesis:
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:

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:

let x be object ; :: thesis:
assume A52: x in { x where x is Element of NAT : ( x in z & x < i ) } /\ {i} ; :: thesis:
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:

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 ;

now :: thesis:

assume i in y ; :: thesis:
then not i in {i} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

hence not i in y ; :: thesis:

A58: now :: thesis:

let m, n be Nat; :: thesis:
assume m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} ; :: thesis:
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:
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:

end;

A61: now :: thesis:

let m, n be Nat; :: thesis:
assume m in { x where x is Element of NAT : ( x in z & x < i ) } ; :: thesis:
then A62: ex x9 being Element of NAT st
( m = x9 & x9 in z & x9 < i ) ;
assume n in {i} ; :: thesis:
hence m < n by A62, TARSKI:def 1; :: thesis:

end;

A63: now :: thesis:

let m, n be Nat; :: thesis:
assume m in { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} ; :: thesis:
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:
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:

end;

A66: now :: thesis:

let m, n be Nat; :: thesis:
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:
then A68: ex x9 being Element of NAT st
( m = x9 & x9 in z & x9 < i ) ;
assume n in {(i + 1)} ; :: thesis:
then n = i + 1 by TARSKI:def 1;
hence m < n by A68, A67, XXREAL_0:2; :: thesis:

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;
then bbb: { x where x is Element of NAT : ( x in z & x < i ) } is included_in_Seg ;
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 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 { x where x is Element of NAT : ( x in z & x < i ) } \/ {i} is included_in_Seg ;
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 a46, A45, A58, FINSEQ_3:42;
{i} c= z by A45, XBOOLE_1:7, XBOOLE_1:11;
then {i} c= Seg (k + 1) by A42;
then {i} is included_in_Seg ;
then A71: Sgm ( { x where x is Element of NAT : ( x in z & x ) ^ (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 { x where x is Element of NAT : ( x in z & x < i ) } \/ {(i + 1)} is included_in_Seg ;
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 a46, A55, A63, FINSEQ_3:42;
then A74: Sgm y = ((Sgm { x where x is Element of NAT : ( x in z & x ) ^ (Sgm { x where x is Element of NAT : ( x in z & i + 1 < x ) } ) by A69, FINSEQ_3:44;

A75: now :: thesis:

let x be set ; :: thesis:
A76: len ((Sgm { x where x is Element of NAT : ( x in z & x ) = (len (Sgm { x where x is Element of NAT : ( x in z & x ) by FINSEQ_1:22
.= (len (Sgm { x where x is Element of NAT : ( x in z & x ) by FINSEQ_1:40
.= len ((Sgm { x where x is Element of NAT : ( x in z & x ) by FINSEQ_1:22 ;
assume A77: x in dom (Sgm z) ; :: thesis:
then reconsider x9 = x as Element of NAT ;
A78: dom ((Sgm { x where x is Element of NAT : ( x in z & x ) = Seg (len ((Sgm { x where x is Element of NAT : ( x in z & x )) by FINSEQ_1:def 3
.= dom ((Sgm { x where x is Element of NAT : ( x in z & x ) by A76, FINSEQ_1:def 3 ;

per cases by A72, A77, FINSEQ_1:25;

suppose A79: x9 in dom ((Sgm { x where x is Element of NAT : ( x in z & x ) ; :: thesis:

per cases by A79, FINSEQ_1:25;

suppose A80: x9 in dom (Sgm { x where x is Element of NAT : ( x in z & x < i ) } ) ; :: thesis:

then A81: (Sgm { x where x is Element of NAT : ( x in z & x ) . x9 by FINSEQ_1:def 7
.= (((Sgm { x where x is Element of NAT : ( x in z & x ) ^ (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 ) . x9 by A80, FINSEQ_1:def 7
.= (((Sgm { x where x is Element of NAT : ( x in z & x ) ^ (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:
thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis:

proof

assume (Sgm z) . x = i ; :: thesis:
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 bbb, FINSEQ_1:def 14;
then ex x999 being Element of NAT st
( x999 = i & x999 in z & x999 < i ) ;
hence (Sgm y) . x = i + 1 ; :: thesis:

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:

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 . x99
.= ((Sgm { x where x is Element of NAT : ( x in z & x ) . x9 by A82, A83, FINSEQ_1:def 7
.= (((Sgm { x where x is Element of NAT : ( x in z & x ) ^ (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:
thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis:

proof

assume (Sgm z) . x = i ; :: thesis:
A86: x99 in dom <*(i + 1)*> by A84, FINSEQ_1:38;
i + 1 = <*(i + 1)*> . x99 by A85
.= ((Sgm { x where x is Element of NAT : ( x in z & x ) . x9 by A83, A86, FINSEQ_1:def 7
.= (((Sgm { x where x is Element of NAT : ( x in z & x ) ^ (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:

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 )) + x99 ) ; :: thesis:

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 )) + 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:
thus ( (Sgm z) . x = i implies (Sgm y) . x = i + 1 ) :: thesis:

proof

assume (Sgm z) . x = i ; :: thesis:
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 a46, FINSEQ_1:def 14;
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:

end;

rng (Sgm z) c= dom s1 by a9, A9, FINSEQ_1:def 14;
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:

let x be object ; :: thesis:
assume A91: x in dom (s1 * (Sgm y)) ; :: thesis:
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 ) . x = i or (Sgm z) . x <> i ) ;

suppose A94: (Sgm z) . x = i ; :: thesis:

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

end;

suppose A95: (Sgm z) . x <> i ; :: thesis:

(s1 * (Sgm y)) . x = s1 . ((Sgm y) . x) by A91, FUNCT_1:12
.= s1 . ((Sgm z) . x) by A75, A92, A95
.= (s1 * (Sgm z)) . x by A93, FUNCT_1:12 ;
hence (s1 * (Sgm y)) . x = (s1 * (Sgm z)) . x ; :: thesis:

end;