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

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) )

hence
the_schreier_series_of (s1,s2) is_finer_than s1
; :: thesis: verum( 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 ) } ;

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;

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)

then A31: dom s1 c= dom f by FINSEQ_1: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:113;

then A36: dom s1 = dom ((the_schreier_series_of (s1,s2)) * f) by A18, A34, RELAT_1:27;

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;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]

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;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;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

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

y in REAL

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;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

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

y1 = y2

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;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

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

x in NAT

then A13:
dom g c= NAT
;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;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

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

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

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

then A30:
Seg (len s1) c= dom f
;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;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

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

then
dom f c= dom s1
;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;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

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

s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x

let x be object ; :: thesis: ( x in dom s1 implies s1 . b_{1} = ((the_schreier_series_of (s1,s2)) * f) . b_{1} )

assume A38: x in dom s1 ; :: thesis: s1 . b_{1} = ((the_schreier_series_of (s1,s2)) * f) . b_{1}

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;

end;assume A38: x in dom s1 ; :: thesis: s1 . 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 )
;

end;

suppose A43:
i = len s1
; :: thesis: s1 . b_{1} = ((the_schreier_series_of (s1,s2)) * f) . b_{1}

((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;.= (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

suppose
i <> len s1
; :: thesis: s1 . b_{1} = ((the_schreier_series_of (s1,s2)) * f) . b_{1}

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;

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;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)

then
the carrier of H2 c= the carrier of ((Omega). G)
;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;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

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

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

then A58:
f | (Seg (len s1)) is increasing
by RFUNCT_2:20;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;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

now :: thesis: for y being object st y in f .: (Seg (len s1)) holds

y in NAT \ {0}

then
f .: (Seg (len s1)) c= NAT \ {0}
;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;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

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