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

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

let x be set ; :: 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 set 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 set 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 set ;
take y = y; :: thesis: ex z being set 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

let y be set ; :: thesis: ( y in rng g implies y in REAL )
assume y in rng g ; :: thesis: y in REAL
then consider x being set such that
A5: [x,y] in g by RELAT_1:def 5;
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, ZFMISC_1:33;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

A7: now

let x, y1, y2 be set ; :: 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, ZFMISC_1:33;
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, ZFMISC_1:33;
hence y1 = y2 by A8, A10, A9, ZFMISC_1:33; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom g implies x in NAT )
assume x in dom g ; :: thesis: x in NAT
then consider y being set such that
A11: [x,y] in g by RELAT_1:def 4;
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, ZFMISC_1:33;
hence x in NAT ; :: thesis: verum

end;

then A13: dom g c= NAT by TARSKI:def 3;
reconsider g = g as Function by A7, FUNCT_1:def 1;
A14: rng g c= REAL by A4, TARSKI:def 3;
reconsider f = g as PartFunc of (dom g),(rng g) by RELSET_1:11;
dom g c= REAL by A13, XBOOLE_1:1;
then reconsider f = f as PartFunc of REAL ,REAL by A14, RELSET_1:17;
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:3;
A15: (id (dom s1)) * R = R by FUNCT_2:23;
(len s2) + 1 > 1 + 1 by A2, XREAL_1:8;
then len s2 >= 2 by NAT_1:13;
then A16: (len s2) - 1 >= 2 - 1 by XREAL_1:11;
(len s1) + 1 > 1 + 1 by A1, XREAL_1:8;
then len s1 >= 2 by NAT_1:13;
then (len s1) - 1 >= 2 - 1 by XREAL_1:11;
then reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by A16, INT_1:16;
A17: len (the_schreier_series_of s1,s2) = l by A1, A2, Def38;
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:8;
then len s2 >= 2 by NAT_1:13;
then A19: (len s2) - 1 >= 2 - 1 by XREAL_1:11;

now

let y be set ; :: thesis: ( y in fX implies y in Seg l )
assume y in fX ; :: thesis: y in Seg l
then consider x being set 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 number by A21, ZFMISC_1:33;
A24: k - 1 >= 1 - 1 by A22, XREAL_1:11;
then A25: y9 > 0 by A19, A21, ZFMISC_1:33;
k - 1 <= (len s1) - 1 by A23, XREAL_1:11;
then A26: (k - 1) * ((len s2) - 1) <= ((len s1) - 1) * ((len s2) - 1) by A19, XREAL_1:66;
((k - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by A19, A24, XREAL_1:8;
then A27: y9 >= 1 by A21, ZFMISC_1:33;
reconsider y9 = y9 as Element of NAT by A25, INT_1:16;
((k - 1) * ((len s2) - 1)) + 1 = y by A21, ZFMISC_1:33;
then y9 <= l by A26, XREAL_1:8;
hence y in Seg l by A27; :: thesis: verum

end;

then A28: fX c= Seg l by TARSKI:def 3;
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

let x be set ; :: 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:3;
then [x,(((k - 1) * ((len s2) - 1)) + 1)] in f ;
hence x in dom f by RELAT_1:def 4; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in dom f implies x in dom s1 )
assume x in dom f ; :: thesis: x in dom s1
then consider y being set such that
A32: [x,y] in f by RELAT_1:def 4;
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, ZFMISC_1:33;
hence x in dom s1 by FINSEQ_1:def 3; :: thesis: verum

end;

then dom f c= dom s1 by TARSKI:def 3;
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:146;
then A36: dom s1 = dom ((the_schreier_series_of s1,s2) * f) by A18, A34, RELAT_1:46;

A37: now

let x be set ; :: 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 4;
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, ZFMISC_1:33;
then ((i - 1) * ((len s2) - 1)) + 1 in rng f by A31, A38, FUNCT_1:12;
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:46;

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:22
.= (the_schreier_series_of s1,s2) . k by A39, ZFMISC_1:33
.= (1). G by A1, A2, A43, Def38
.= s1 . (len s1) by Def31 ;
hence s1 . x = ((the_schreier_series_of s1,s2) * f) . x by A39, A43, ZFMISC_1:33; :: 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:11;
A46: s2 . 1 = (Omega). G by Def31;
then reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . 1 as strict StableSubgroup of G by A40, A45, Th111;

now

let x be set ; :: 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) by TARSKI:def 3;
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:11;
then A49: (len s2) - 1 >= 0 + 1 by INT_1:20;
0 + i <= 1 + i by XREAL_1:8;
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, Def31;
((the_schreier_series_of s1,s2) * f) . x = (the_schreier_series_of s1,s2) . (f . x) by A42, FUNCT_1:22
.= (the_schreier_series_of s1,s2) . k by A39, ZFMISC_1:33
.= H1 "\/" (H2 /\ H3) by A1, A2, A40, A45, A49, Def38
.= H1 "\/" H2 by A48, Th18
.= H2 by A51, Th36 ;
hence s1 . x = ((the_schreier_series_of s1,s2) * f) . x by A39, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

now

let r1, r2 be Element of 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:8;
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:8;
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, ZFMISC_1:33;
assume A55: r1 < r2 ; :: thesis: f . r1 < f . r2
k9 = r1 by A52, ZFMISC_1:33;
then k9 - 1 < k99 - 1 by A55, A54, XREAL_1:11;
then A56: (k9 - 1) * ((len s2) - 1) < (k99 - 1) * ((len s2) - 1) by A19, XREAL_1:70;
A57: ((k99 - 1) * ((len s2) - 1)) + 1 = f . r2 by A53, ZFMISC_1:33;
((k9 - 1) * ((len s2) - 1)) + 1 = f . r1 by A52, ZFMISC_1:33;
hence f . r1 < f . r2 by A57, A56, XREAL_1:8; :: thesis: verum

end;

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

now

let y be set ; :: 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 set 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 number by A60, ZFMISC_1:33;
( ((k - 1) * ((len s2) - 1)) + 1 = y & k - 1 >= 1 - 1 ) by A60, A61, XREAL_1:11, ZFMISC_1:33;
then ( y9 in NAT & not y in {0 } ) by A19, INT_1:16, TARSKI:def 1;
hence y in NAT \ {0 } by XBOOLE_0:def 5; :: thesis: verum

end;

then f .: (Seg (len s1)) c= NAT \ {0 } by TARSKI:def 3;
then (the_schreier_series_of s1,s2) * (Sgm fX) = (the_schreier_series_of s1,s2) * (f * (Sgm (Seg (len s1)))) by A30, A58, Lm38
.= ((the_schreier_series_of s1,s2) * f) * (Sgm (Seg (len s1))) by RELAT_1:55
.= s1 * (Sgm (Seg (len s1))) by A36, A37, FUNCT_1:9
.= s1 * (idseq (len s1)) by FINSEQ_3:54
.= 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 by Def32; :: thesis: verum