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 A1: ( len s1 > 1 & len s2 > 1 ) ; :: thesis: the_schreier_series_of s1,s2 is_finer_than s1

now

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
A2: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = x & 1 <= k & k <= len s1 ) ;
set y = k;
set z = ((k - 1) * ((len s2) - 1)) + 1;
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 A2; :: 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;

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
A3: [x,y] in g by RELAT_1:def 4;
consider k being Element of NAT such that
A4: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A3;
k = x by A4, ZFMISC_1:33;
hence x in NAT ; :: thesis: verum

end;

then A5: dom g c= NAT by TARSKI:def 3;

A6: 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
A7: [x,y] in g by RELAT_1:def 5;
consider k being Element of NAT such that
A8: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A7;
((k - 1) * ((len s2) - 1)) + 1 = y by A8, ZFMISC_1:33;
hence y in REAL by XREAL_0:def 1; :: thesis: verum

end;

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
A9: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y1] & 1 <= k & k <= len s1 ) ;
assume [x,y2] in g ; :: thesis: y1 = y2
then consider k' being Element of NAT such that
A10: ( [k',(((k' - 1) * ((len s2) - 1)) + 1)] = [x,y2] & 1 <= k' & k' <= len s1 ) ;
A11: ( k = x & ((k - 1) * ((len s2) - 1)) + 1 = y1 & 1 <= k & k <= len s1 ) by A9, ZFMISC_1:33;
( k' = x & ((k' - 1) * ((len s2) - 1)) + 1 = y2 & 1 <= k' & k' <= len s1 ) by A10, ZFMISC_1:33;
hence y1 = y2 by A11; :: thesis: verum

end;

then reconsider g = g as Function by FUNCT_1:def 1;
reconsider f = g as PartFunc of (dom g),(rng g) by RELSET_1:11;
( dom g c= REAL & rng g c= REAL ) by A5, A6, TARSKI:def 3, XBOOLE_1:1;
then reconsider f = f as PartFunc of REAL ,REAL by RELSET_1:17;
( (len s1) + 1 > 1 + 1 & (len s2) + 1 > 1 + 1 ) by A1, XREAL_1:8;
then ( len s1 >= 2 & len s2 >= 2 ) by NAT_1:13;
then A12: ( (len s1) - 1 >= 2 - 1 & (len s2) - 1 >= 2 - 1 ) by XREAL_1:11;
set X = Seg (len s1);

now

let x be set ; :: thesis: ( x in Seg (len s1) implies x in dom f )
assume A13: 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;
( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,(((k - 1) * ((len s2) - 1)) + 1)] & 1 <= k & k <= len s1 ) by A13, 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 A14: Seg (len s1) c= dom f by TARSKI:def 3;

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 k' being Element of NAT such that
A15: ( [k',(((k' - 1) * ((len s2) - 1)) + 1)] = [r1,(f . r1)] & 1 <= k' & k' <= 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 k'' being Element of NAT such that
A16: ( [k'',(((k'' - 1) * ((len s2) - 1)) + 1)] = [r2,(f . r2)] & 1 <= k'' & k'' <= len s1 ) ;
assume A17: r1 < r2 ; :: thesis: f . r1 < f . r2
A18: ( k' = r1 & ((k' - 1) * ((len s2) - 1)) + 1 = f . r1 ) by A15, ZFMISC_1:33;
A19: ( k'' = r2 & ((k'' - 1) * ((len s2) - 1)) + 1 = f . r2 ) by A16, ZFMISC_1:33;
then k' - 1 < k'' - 1 by A17, A18, XREAL_1:11;
then (k' - 1) * ((len s2) - 1) < (k'' - 1) * ((len s2) - 1) by A12, XREAL_1:70;
hence f . r1 < f . r2 by A18, A19, XREAL_1:8; :: thesis: verum

end;

then A20: 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
A21: ( [x,y] in g & x in Seg (len s1) ) by RELAT_1:def 13;
consider k being Element of NAT such that
A22: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A21;
A23: ((k - 1) * ((len s2) - 1)) + 1 = y by A22, ZFMISC_1:33;
reconsider y' = y as integer number by A22, ZFMISC_1:33;
k - 1 >= 1 - 1 by A22, XREAL_1:11;
then (k - 1) * ((len s2) - 1) >= 0 * ((len s2) - 1) by A12;
then A24: ((k - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by XREAL_1:8;
then A25: y' in NAT by A23, INT_1:16;
not y in {0 } by A23, A24, TARSKI:def 1;
hence y in NAT \ {0 } by A25, XBOOLE_0:def 5; :: thesis: verum

end;

then A26: f .: (Seg (len s1)) c= NAT \ {0 } by TARSKI:def 3;
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) )
set l = (((len s1) - 1) * ((len s2) - 1)) + 1;
( (len s1) + 1 > 1 + 1 & (len s2) + 1 > 1 + 1 ) by A1, XREAL_1:8;
then ( len s1 >= 2 & len s2 >= 2 ) by NAT_1:13;
then ( (len s1) - 1 >= 2 - 1 & (len s2) - 1 >= 2 - 1 ) by XREAL_1:11;
then ((len s1) - 1) * ((len s2) - 1) >= 0 * ((len s2) - 1) ;
then (((len s1) - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by XREAL_1:8;
then reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by INT_1:16;

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
A27: ( [x,y] in g & x in Seg (len s1) ) by RELAT_1:def 13;
consider k being Element of NAT such that
A28: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A27;
A29: ((k - 1) * ((len s2) - 1)) + 1 = y by A28, ZFMISC_1:33;
reconsider y' = y as integer number by A28, ZFMISC_1:33;
k - 1 >= 1 - 1 by A28, XREAL_1:11;
then (k - 1) * ((len s2) - 1) >= 0 * ((len s2) - 1) by A12;
then A30: ((k - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by XREAL_1:8;
then A31: y' >= 1 by A28, ZFMISC_1:33;
y' > 0 by A28, A30, ZFMISC_1:33;
then reconsider y' = y' as Element of NAT by INT_1:16;
k - 1 <= (len s1) - 1 by A28, XREAL_1:11;
then (k - 1) * ((len s2) - 1) <= ((len s1) - 1) * ((len s2) - 1) by A12, XREAL_1:66;
then y' <= l by A29, XREAL_1:8;
hence y in Seg l by A31; :: thesis: verum

end;

then A32: fX c= Seg l by TARSKI:def 3;
A33: len (the_schreier_series_of s1,s2) = l by A1, Def38;
then A34: dom (the_schreier_series_of s1,s2) = Seg l by FINSEQ_1:def 3;
thus fX c= dom (the_schreier_series_of s1,s2) by A32, A33, FINSEQ_1:def 3; :: thesis: s1 = (the_schreier_series_of s1,s2) * (Sgm fX)
set t = the_schreier_series_of s1,s2;
A35: dom s1 c= dom f by A14, 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
A36: [x,y] in f by RELAT_1:def 4;
consider k being Element of NAT such that
A37: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A36;
( k in Seg (len s1) & k = x ) by A37, 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 A38: dom s1 = dom f by A35, XBOOLE_0:def 10;
then Seg (len s1) = dom f by FINSEQ_1:def 3;
then A39: rng f c= Seg l by A32, RELAT_1:146;
then A40: dom s1 = dom ((the_schreier_series_of s1,s2) * f) by A34, A38, RELAT_1:46;

A41: now

let x be set ; :: thesis: ( x in dom s1 implies s1 . b₁ = ((the_schreier_series_of s1,s2) * f) . b₁ )
assume A42: x in dom s1 ; :: thesis: s1 . b₁ = ((the_schreier_series_of s1,s2) * f) . b₁
then A43: x in dom ((the_schreier_series_of s1,s2) * f) by A34, A38, A39, RELAT_1:46;
[x,(f . x)] in f by A35, A42, FUNCT_1:def 4;
then consider i being Element of NAT such that
A44: ( [i,(((i - 1) * ((len s2) - 1)) + 1)] = [x,(f . x)] & 1 <= i & i <= len s1 ) ;
A45: ( i = x & ((i - 1) * ((len s2) - 1)) + 1 = f . x ) by A44, ZFMISC_1:33;
set k = ((i - 1) * ((len s2) - 1)) + 1;
((i - 1) * ((len s2) - 1)) + 1 in rng f by A35, A42, A45, FUNCT_1:12;
then ((i - 1) * ((len s2) - 1)) + 1 in Seg l by A39;
then reconsider k = ((i - 1) * ((len s2) - 1)) + 1 as Element of NAT ;

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

suppose A46: 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 A43, FUNCT_1:22
.= (the_schreier_series_of s1,s2) . k by A44, ZFMISC_1:33
.= (1). G by A1, A46, Def38
.= s1 . (len s1) by Def31 ;
hence s1 . x = ((the_schreier_series_of s1,s2) * f) . x by A44, A46, 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 A44, XXREAL_0:1;
then A47: i + 1 <= len s1 by NAT_1:13;
then A48: (i + 1) - 1 <= (len s1) - 1 by XREAL_1:11;
(len s2) - 1 > 1 - 1 by A1, XREAL_1:11;
then A49: (len s2) - 1 >= 0 + 1 by INT_1:20;
A50: s2 . 1 = (Omega). G by Def31;
then reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . 1 as strict StableSubgroup of G by A44, A48, Th111;

now

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

end;

then the carrier of H2 c= the carrier of ((Omega). G) by TARSKI:def 3;
then A52: the carrier of H2 = the carrier of H2 /\ the carrier of H3 by A50, XBOOLE_1:28;
0 + i <= 1 + i by XREAL_1:8;
then 1 <= i + 1 by A44, XXREAL_0:2;
then i + 1 in Seg (len s1) by A47;
then A53: i + 1 in dom s1 by FINSEQ_1:def 3;
i in Seg (len s1) by A44;
then i in dom s1 by FINSEQ_1:def 3;
then A54: H1 is normal StableSubgroup of H2 by A53, Def31;
((the_schreier_series_of s1,s2) * f) . x = (the_schreier_series_of s1,s2) . (f . x) by A43, FUNCT_1:22
.= (the_schreier_series_of s1,s2) . k by A44, ZFMISC_1:33
.= H1 "\/" (H2 /\ H3) by A1, A44, A48, A49, Def38
.= H1 "\/" H2 by A52, Th18
.= H2 by A54, Th36 ;
hence s1 . x = ((the_schreier_series_of s1,s2) * f) . x by A44, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

A55: (the_schreier_series_of s1,s2) * (Sgm fX) = (the_schreier_series_of s1,s2) * (f * (Sgm (Seg (len s1)))) by A14, A20, A26, Lm38
.= ((the_schreier_series_of s1,s2) * f) * (Sgm (Seg (len s1))) by RELAT_1:55
.= s1 * (Sgm (Seg (len s1))) by A40, A41, 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 ;
set R = s1;
set dR = dom s1;
set rR = rng s1;
reconsider R = s1 as Relation of (dom s1),(rng s1) by FUNCT_2:3;
(id (dom s1)) * R = R by FUNCT_2:23;
hence s1 = (the_schreier_series_of s1,s2) * (Sgm fX) by A55; :: thesis: verum

end;

hence the_schreier_series_of s1,s2 is_finer_than s1 by Def32; :: thesis: verum