let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1
let s1, s2 be CompositionSeries of G; :: thesis: ( len s1 > 1 & len s2 > 1 implies the_schreier_series_of (s1,s2) is_finer_than s1 )
assume that
A1: len s1 > 1 and
A2: len s2 > 1 ; :: thesis: the_schreier_series_of (s1,s2) is_finer_than s1

now :: thesis: ex fX being Element of bool REAL st
( fX c= dom (the_schreier_series_of (s1,s2)) & s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX) )

set rR = rng s1;
set R = s1;
set l = (((len s1) - 1) * ((len s2) - 1)) + 1;
set X = Seg (len s1);
set g = { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } ;

now :: thesis: for x being object st x in { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } holds
ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } implies ex y, z being object st x = [y,z] )
assume x in { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } ; :: thesis: ex y, z being object st x = [y,z]
then consider k being Element of NAT such that
A3: [k,(((k - 1) * ((len s2) - 1)) + 1)] = x and
1 <= k and
k <= len s1 ;
set z = ((k - 1) * ((len s2) - 1)) + 1;
set y = k;
reconsider y = k, z = ((k - 1) * ((len s2) - 1)) + 1 as object ;
take y = y; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A3; :: thesis: verum

end;

then reconsider g = { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } as Relation by RELAT_1:def 1;

A4: now :: thesis: for y being object st y in rng g holds
y in REAL

let y be object ; :: thesis: ( y in rng g implies y in REAL )
assume y in rng g ; :: thesis: y in REAL
then consider x being object such that
A5: [x,y] in g by XTUPLE_0:def 13;
consider k being Element of NAT such that
A6: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
1 <= k and
k <= len s1 by A5;
((k - 1) * ((len s2) - 1)) + 1 = y by A6, XTUPLE_0:1;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

A7: now :: thesis: for x, y1, y2 being object st [x,y1] in g & [x,y2] in g holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in g & [x,y2] in g implies y1 = y2 )
assume [x,y1] in g ; :: thesis: ( [x,y2] in g implies y1 = y2 )
then consider k being Element of NAT such that
A8: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y1] and
1 <= k and
k <= len s1 ;
A9: k = x by A8, XTUPLE_0:1;
assume [x,y2] in g ; :: thesis: y1 = y2
then consider k9 being Element of NAT such that
A10: [k9,(((k9 - 1) * ((len s2) - 1)) + 1)] = [x,y2] and
1 <= k9 and
k9 <= len s1 ;
k9 = x by A10, XTUPLE_0:1;
hence y1 = y2 by A8, A10, A9, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: for x being object st x in dom g holds
x in NAT

let x be object ; :: thesis: ( x in dom g implies x in NAT )
assume x in dom g ; :: thesis: x in NAT
then consider y being object such that
A11: [x,y] in g by XTUPLE_0:def 12;
consider k being Element of NAT such that
A12: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
1 <= k and
k <= len s1 by A11;
k = x by A12, XTUPLE_0:1;
hence x in NAT ; :: thesis: verum

end;

then A13: dom g c= NAT ;
reconsider g = g as Function by A7, FUNCT_1:def 1;
A14: rng g c= REAL by A4;
reconsider f = g as PartFunc of (dom g),(rng g) by RELSET_1:4;
dom g c= REAL by A13, NUMBERS:19;
then reconsider f = f as PartFunc of REAL,REAL by A14, RELSET_1:7;
set dR = dom s1;
set t = the_schreier_series_of (s1,s2);
set fX = f .: (Seg (len s1));
take fX = f .: (Seg (len s1)); :: thesis: ( fX c= dom (the_schreier_series_of (s1,s2)) & s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX) )
reconsider R = s1 as Relation of (dom s1),(rng s1) by FUNCT_2:1;
A15: (id (dom s1)) * R = R by FUNCT_2:17;
(len s2) + 1 > 1 + 1 by A2, XREAL_1:6;
then len s2 >= 2 by NAT_1:13;
then A16: (len s2) - 1 >= 2 - 1 by XREAL_1:9;
(len s1) + 1 > 1 + 1 by A1, XREAL_1:6;
then len s1 >= 2 by NAT_1:13;
then (len s1) - 1 >= 2 - 1 by XREAL_1:9;
then reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by A16, INT_1:3;
A17: len (the_schreier_series_of (s1,s2)) = l by A1, A2, Def35;
then A18: dom (the_schreier_series_of (s1,s2)) = Seg l by FINSEQ_1:def 3;
(len s2) + 1 > 1 + 1 by A2, XREAL_1:6;
then len s2 >= 2 by NAT_1:13;
then A19: (len s2) - 1 >= 2 - 1 by XREAL_1:9;

now :: thesis: for y being object st y in fX holds
y in Seg l

let y be object ; :: thesis: ( y in fX implies y in Seg l )
assume y in fX ; :: thesis: y in Seg l
then consider x being object such that
A20: [x,y] in g and
x in Seg (len s1) by RELAT_1:def 13;
consider k being Element of NAT such that
A21: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
A22: 1 <= k and
A23: k <= len s1 by A20;
reconsider y9 = y as Integer by A21, XTUPLE_0:1;
A24: k - 1 >= 1 - 1 by A22, XREAL_1:9;
then A25: y9 > 0 by A19, A21, XTUPLE_0:1;
k - 1 <= (len s1) - 1 by A23, XREAL_1:9;
then A26: (k - 1) * ((len s2) - 1) <= ((len s1) - 1) * ((len s2) - 1) by A19, XREAL_1:64;
((k - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by A19, A24, XREAL_1:6;
then A27: y9 >= 1 by A21, XTUPLE_0:1;
reconsider y9 = y9 as Element of NAT by A25, INT_1:3;
((k - 1) * ((len s2) - 1)) + 1 = y by A21, XTUPLE_0:1;
then y9 <= l by A26, XREAL_1:6;
hence y in Seg l by A27; :: thesis: verum

end;

then A28: fX c= Seg l ;
hence fX c= dom (the_schreier_series_of (s1,s2)) by A17, FINSEQ_1:def 3; :: thesis: s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX)

now :: thesis: for x being object st x in Seg (len s1) holds
x in dom f

let x be object ; :: thesis: ( x in Seg (len s1) implies x in dom f )
assume A29: x in Seg (len s1) ; :: thesis: x in dom f
then reconsider k = x as Element of NAT ;
set y = ((k - 1) * ((len s2) - 1)) + 1;
( 1 <= k & k <= len s1 ) by A29, FINSEQ_1:1;
then [x,(((k - 1) * ((len s2) - 1)) + 1)] in f ;
hence x in dom f by XTUPLE_0:def 12; :: thesis: verum

end;

then A30: Seg (len s1) c= dom f ;
then A31: dom s1 c= dom f by FINSEQ_1:def 3;

now :: thesis: for x being object st x in dom f holds
x in dom s1

let x be object ; :: thesis: ( x in dom f implies x in dom s1 )
assume x in dom f ; :: thesis: x in dom s1
then consider y being object such that
A32: [x,y] in f by XTUPLE_0:def 12;
consider k being Element of NAT such that
A33: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A32;
( k in Seg (len s1) & k = x ) by A33, XTUPLE_0:1;
hence x in dom s1 by FINSEQ_1:def 3; :: thesis: verum

end;

then dom f c= dom s1 ;
then A34: dom s1 = dom f by A31, XBOOLE_0:def 10;
then Seg (len s1) = dom f by FINSEQ_1:def 3;
then A35: rng f c= Seg l by A28, RELAT_1:113;
then A36: dom s1 = dom ((the_schreier_series_of (s1,s2)) * f) by A18, A34, RELAT_1:27;

A37: now :: thesis: for x being object st x in dom s1 holds
s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x

let x be object ; :: thesis: ( x in dom s1 implies s1 . b₁ = ((the_schreier_series_of (s1,s2)) * f) . b₁ )
assume A38: x in dom s1 ; :: thesis: s1 . b₁ = ((the_schreier_series_of (s1,s2)) * f) . b₁
then [x,(f . x)] in f by A31, FUNCT_1:def 2;
then consider i being Element of NAT such that
A39: [i,(((i - 1) * ((len s2) - 1)) + 1)] = [x,(f . x)] and
A40: 1 <= i and
A41: i <= len s1 ;
set k = ((i - 1) * ((len s2) - 1)) + 1;
((i - 1) * ((len s2) - 1)) + 1 = f . x by A39, XTUPLE_0:1;
then ((i - 1) * ((len s2) - 1)) + 1 in rng f by A31, A38, FUNCT_1:3;
then ((i - 1) * ((len s2) - 1)) + 1 in Seg l by A35;
then reconsider k = ((i - 1) * ((len s2) - 1)) + 1 as Element of NAT ;
A42: x in dom ((the_schreier_series_of (s1,s2)) * f) by A18, A34, A35, A38, RELAT_1:27;

per cases ( i = len s1 or i <> len s1 ) ;

suppose A43: i = len s1 ; :: thesis: s1 . b₁ = ((the_schreier_series_of (s1,s2)) * f) . b₁

((the_schreier_series_of (s1,s2)) * f) . x = (the_schreier_series_of (s1,s2)) . (f . x) by A42, FUNCT_1:12
.= (the_schreier_series_of (s1,s2)) . k by A39, XTUPLE_0:1
.= (1). G by A1, A2, A43, Def35
.= s1 . (len s1) by Def28 ;
hence s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x by A39, A43, XTUPLE_0:1; :: thesis: verum

end;

suppose i <> len s1 ; :: thesis: s1 . b₁ = ((the_schreier_series_of (s1,s2)) * f) . b₁

then i < len s1 by A41, XXREAL_0:1;
then A44: i + 1 <= len s1 by NAT_1:13;
then A45: (i + 1) - 1 <= (len s1) - 1 by XREAL_1:9;
A46: s2 . 1 = (Omega). G by Def28;
then reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . 1 as strict StableSubgroup of G by A40, A45, Th111;

now :: thesis: for x being object st x in the carrier of H2 holds
x in the carrier of ((Omega). G)

let x be object ; :: thesis: ( x in the carrier of H2 implies x in the carrier of ((Omega). G) )
H2 is Subgroup of G by Def7;
then A47: the carrier of H2 c= the carrier of G by GROUP_2:def 5;
assume x in the carrier of H2 ; :: thesis: x in the carrier of ((Omega). G)
hence x in the carrier of ((Omega). G) by A47; :: thesis: verum

end;

then the carrier of H2 c= the carrier of ((Omega). G) ;
then A48: the carrier of H2 = the carrier of H2 /\ the carrier of H3 by A46, XBOOLE_1:28;
(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;
then A49: (len s2) - 1 >= 0 + 1 by INT_1:7;
0 + i <= 1 + i by XREAL_1:6;
then 1 <= i + 1 by A40, XXREAL_0:2;
then i + 1 in Seg (len s1) by A44;
then A50: i + 1 in dom s1 by FINSEQ_1:def 3;
i in Seg (len s1) by A40, A41;
then i in dom s1 by FINSEQ_1:def 3;
then A51: H1 is normal StableSubgroup of H2 by A50, Def28;
((the_schreier_series_of (s1,s2)) * f) . x = (the_schreier_series_of (s1,s2)) . (f . x) by A42, FUNCT_1:12
.= (the_schreier_series_of (s1,s2)) . k by A39, XTUPLE_0:1
.= H1 "\/" (H2 /\ H3) by A1, A2, A40, A45, A49, Def35
.= H1 "\/" H2 by A48, Th18
.= H2 by A51, Th36 ;
hence s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x by A39, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

now :: thesis: for r1, r2 being Real st r1 in (Seg (len s1)) /\ (dom f) & r2 in (Seg (len s1)) /\ (dom f) & r1 < r2 holds
f . r1 < f . r2

let r1, r2 be Real; :: thesis: ( r1 in (Seg (len s1)) /\ (dom f) & r2 in (Seg (len s1)) /\ (dom f) & r1 < r2 implies f . r1 < f . r2 )
assume r1 in (Seg (len s1)) /\ (dom f) ; :: thesis: ( r2 in (Seg (len s1)) /\ (dom f) & r1 < r2 implies f . r1 < f . r2 )
then r1 in dom f by XBOOLE_0:def 4;
then [r1,(f . r1)] in f by FUNCT_1:1;
then consider k9 being Element of NAT such that
A52: [k9,(((k9 - 1) * ((len s2) - 1)) + 1)] = [r1,(f . r1)] and
1 <= k9 and
k9 <= len s1 ;
assume r2 in (Seg (len s1)) /\ (dom f) ; :: thesis: ( r1 < r2 implies f . r1 < f . r2 )
then r2 in dom f by XBOOLE_0:def 4;
then [r2,(f . r2)] in f by FUNCT_1:1;
then consider k99 being Element of NAT such that
A53: [k99,(((k99 - 1) * ((len s2) - 1)) + 1)] = [r2,(f . r2)] and
1 <= k99 and
k99 <= len s1 ;
A54: k99 = r2 by A53, XTUPLE_0:1;
assume A55: r1 < r2 ; :: thesis: f . r1 < f . r2
k9 = r1 by A52, XTUPLE_0:1;
then k9 - 1 < k99 - 1 by A55, A54, XREAL_1:9;
then A56: (k9 - 1) * ((len s2) - 1) < (k99 - 1) * ((len s2) - 1) by A19, XREAL_1:68;
A57: ((k99 - 1) * ((len s2) - 1)) + 1 = f . r2 by A53, XTUPLE_0:1;
((k9 - 1) * ((len s2) - 1)) + 1 = f . r1 by A52, XTUPLE_0:1;
hence f . r1 < f . r2 by A57, A56, XREAL_1:6; :: thesis: verum

end;

then A58: f | (Seg (len s1)) is increasing by RFUNCT_2:20;

now :: thesis: for y being object st y in f .: (Seg (len s1)) holds
y in NAT \ {0}

let y be object ; :: thesis: ( y in f .: (Seg (len s1)) implies y in NAT \ {0} )
assume y in f .: (Seg (len s1)) ; :: thesis: y in NAT \ {0}
then consider x being object such that
A59: [x,y] in g and
x in Seg (len s1) by RELAT_1:def 13;
consider k being Element of NAT such that
A60: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
A61: 1 <= k and
k <= len s1 by A59;
reconsider y9 = y as Integer by A60, XTUPLE_0:1;
( ((k - 1) * ((len s2) - 1)) + 1 = y & k - 1 >= 1 - 1 ) by A60, A61, XREAL_1:9, XTUPLE_0:1;
then ( y9 in NAT & not y in {0} ) by A19, INT_1:3, TARSKI:def 1;
hence y in NAT \ {0} by XBOOLE_0:def 5; :: thesis: verum

end;

then f .: (Seg (len s1)) c= NAT \ {0} ;
then (the_schreier_series_of (s1,s2)) * (Sgm fX) = (the_schreier_series_of (s1,s2)) * (f * (Sgm (Seg (len s1)))) by A30, A58, Lm37
.= ((the_schreier_series_of (s1,s2)) * f) * (Sgm (Seg (len s1))) by RELAT_1:36
.= s1 * (Sgm (Seg (len s1))) by A36, A37, FUNCT_1:2
.= s1 * (idseq (len s1)) by FINSEQ_3:48
.= s1 * (id (Seg (len s1))) by FINSEQ_2:def 1
.= s1 * (id (dom s1)) by FINSEQ_1:def 3 ;
hence s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX) by A15; :: thesis: verum

end;

hence the_schreier_series_of (s1,s2) is_finer_than s1 ; :: thesis: verum