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_equivalent_with the_schreier_series_of (s2,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_equivalent_with the_schreier_series_of (s2,s1)

let s1, s2 be CompositionSeries of G; :: thesis: ( len s1 > 1 & len s2 > 1 implies the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) )

assume that

A1: len s1 > 1 and

A2: len s2 > 1 ; :: thesis: the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1)

set s21 = the_schreier_series_of (s2,s1);

A3: ( (len s1) - 1 > 1 - 1 & (len s2) - 1 > 1 - 1 ) by A1, A2, XREAL_1:9;

set s12 = the_schreier_series_of (s1,s2);

A4: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

A5: len (the_schreier_series_of (s2,s1)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

then A6: not the_schreier_series_of (s2,s1) is empty by A3;

((len s1) - 1) * ((len s2) - 1) > 0 * ((len s2) - 1) by A3, XREAL_1:68;

then A7: (((len s1) - 1) * ((len s2) - 1)) + 1 > 0 + 1 by XREAL_1:6;

hence the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) by A6, A8, Th108; :: thesis: verum

for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds

the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,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_equivalent_with the_schreier_series_of (s2,s1)

let s1, s2 be CompositionSeries of G; :: thesis: ( len s1 > 1 & len s2 > 1 implies the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) )

assume that

A1: len s1 > 1 and

A2: len s2 > 1 ; :: thesis: the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1)

set s21 = the_schreier_series_of (s2,s1);

A3: ( (len s1) - 1 > 1 - 1 & (len s2) - 1 > 1 - 1 ) by A1, A2, XREAL_1:9;

set s12 = the_schreier_series_of (s1,s2);

A4: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

A5: len (the_schreier_series_of (s2,s1)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

then A6: not the_schreier_series_of (s2,s1) is empty by A3;

((len s1) - 1) * ((len s2) - 1) > 0 * ((len s2) - 1) by A3, XREAL_1:68;

then A7: (((len s1) - 1) * ((len s2) - 1)) + 1 > 0 + 1 by XREAL_1:6;

A8: now :: thesis: ex p being Permutation of (dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) st the_series_of_quotients_of (the_schreier_series_of (s1,s2)), the_series_of_quotients_of (the_schreier_series_of (s2,s1)) are_equivalent_under p,O

not the_schreier_series_of (s1,s2) is empty
by A3, A4;set p = { [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] where i, j is Element of NAT : ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) } ;

set X = dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)));

set f1 = the_series_of_quotients_of (the_schreier_series_of (s1,s2));

set f2 = the_series_of_quotients_of (the_schreier_series_of (s2,s1));

A16: len (the_schreier_series_of (s1,s2)) > 1 by A1, A2, A7, Def35;

then A17: (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) + 1 = len (the_schreier_series_of (s1,s2)) by Def33;

A18: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

A26: dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) = Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by FINSEQ_1:def 3;

then A37: rng p = dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A25, XBOOLE_0:def 10;

then A42: dom p = dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A32, XBOOLE_0:def 10;

then reconsider p = p as Function of (dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))),(dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A37, FUNCT_2:1;

A43: p is onto by A37;

then reconsider p = p as Permutation of (dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A43;

take p = p; :: thesis: the_series_of_quotients_of (the_schreier_series_of (s1,s2)), the_series_of_quotients_of (the_schreier_series_of (s2,s1)) are_equivalent_under p,O

A55: len (the_schreier_series_of (s2,s1)) > 1 by A1, A2, A7, Def35;

then A56: (len (the_series_of_quotients_of (the_schreier_series_of (s2,s1)))) + 1 = len (the_schreier_series_of (s2,s1)) by Def33;

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

ex y, z being object st x = [y,z]

then reconsider p = { [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] where i, j is Element of NAT : ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) } as Relation by RELAT_1:def 1;ex y, z being object st x = [y,z]

let x be object ; :: thesis: ( x in { [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] where i, j is Element of NAT : ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) } implies ex y, z being object st x = [y,z] )

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

then consider i, j being Element of NAT such that

A9: [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] = x and

1 <= i and

i <= (len s1) - 1 and

1 <= j and

j <= (len s2) - 1 ;

set z = ((i - 1) * ((len s2) - 1)) + j;

set y = ((j - 1) * ((len s1) - 1)) + i;

reconsider y = ((j - 1) * ((len s1) - 1)) + i, z = ((i - 1) * ((len s2) - 1)) + j 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 A9; :: thesis: verum

end;assume x in { [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] where i, j is Element of NAT : ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) } ; :: thesis: ex y, z being object st x = [y,z]

then consider i, j being Element of NAT such that

A9: [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] = x and

1 <= i and

i <= (len s1) - 1 and

1 <= j and

j <= (len s2) - 1 ;

set z = ((i - 1) * ((len s2) - 1)) + j;

set y = ((j - 1) * ((len s1) - 1)) + i;

reconsider y = ((j - 1) * ((len s1) - 1)) + i, z = ((i - 1) * ((len s2) - 1)) + j 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 A9; :: thesis: verum

set X = dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)));

set f1 = the_series_of_quotients_of (the_schreier_series_of (s1,s2));

set f2 = the_series_of_quotients_of (the_schreier_series_of (s2,s1));

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

y1 = y2

then reconsider p = p as Function by FUNCT_1:def 1;y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in p & [x,y2] in p implies y1 = y2 )

assume [x,y1] in p ; :: thesis: ( [x,y2] in p implies y1 = y2 )

then consider i1, j1 being Element of NAT such that

A10: [(((j1 - 1) * ((len s1) - 1)) + i1),(((i1 - 1) * ((len s2) - 1)) + j1)] = [x,y1] and

A11: ( 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 ) and

j1 <= (len s2) - 1 ;

A12: ((j1 - 1) * ((len s1) - 1)) + i1 = x by A10, XTUPLE_0:1;

assume [x,y2] in p ; :: thesis: y1 = y2

then consider i2, j2 being Element of NAT such that

A13: [(((j2 - 1) * ((len s1) - 1)) + i2),(((i2 - 1) * ((len s2) - 1)) + j2)] = [x,y2] and

A14: ( 1 <= i2 & i2 <= (len s1) - 1 & 1 <= j2 ) and

j2 <= (len s2) - 1 ;

A15: ((j2 - 1) * ((len s1) - 1)) + i2 = x by A13, XTUPLE_0:1;

then j1 = j2 by A1, A11, A14, A12, Lm45;

hence y1 = y2 by A10, A13, A12, A15, XTUPLE_0:1; :: thesis: verum

end;assume [x,y1] in p ; :: thesis: ( [x,y2] in p implies y1 = y2 )

then consider i1, j1 being Element of NAT such that

A10: [(((j1 - 1) * ((len s1) - 1)) + i1),(((i1 - 1) * ((len s2) - 1)) + j1)] = [x,y1] and

A11: ( 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 ) and

j1 <= (len s2) - 1 ;

A12: ((j1 - 1) * ((len s1) - 1)) + i1 = x by A10, XTUPLE_0:1;

assume [x,y2] in p ; :: thesis: y1 = y2

then consider i2, j2 being Element of NAT such that

A13: [(((j2 - 1) * ((len s1) - 1)) + i2),(((i2 - 1) * ((len s2) - 1)) + j2)] = [x,y2] and

A14: ( 1 <= i2 & i2 <= (len s1) - 1 & 1 <= j2 ) and

j2 <= (len s2) - 1 ;

A15: ((j2 - 1) * ((len s1) - 1)) + i2 = x by A13, XTUPLE_0:1;

then j1 = j2 by A1, A11, A14, A12, Lm45;

hence y1 = y2 by A10, A13, A12, A15, XTUPLE_0:1; :: thesis: verum

A16: len (the_schreier_series_of (s1,s2)) > 1 by A1, A2, A7, Def35;

then A17: (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) + 1 = len (the_schreier_series_of (s1,s2)) by Def33;

A18: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

now :: thesis: for y being object st y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) holds

y in rng p

then A25:
dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) c= rng p
;y in rng p

set l9 = ((len s1) - 1) * ((len s2) - 1);

reconsider l9 = ((len s1) - 1) * ((len s2) - 1) as Element of NAT by A3, INT_1:3;

let y be object ; :: thesis: ( y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) implies y in rng p )

assume A19: y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ; :: thesis: y in rng p

then reconsider k = y as Element of NAT ;

A20: y in Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A19, FINSEQ_1:def 3;

then A21: 1 <= k by FINSEQ_1:1;

A22: k <= ((len s1) - 1) * ((len s2) - 1) by A17, A18, A20, FINSEQ_1:1;

0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;

then k <= l9 + 1 by A22, XXREAL_0:2;

then A23: k in Seg (l9 + 1) by A21;

k <> l9 + 1 by A22, NAT_1:13;

then consider i, j being Nat such that

A24: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) by A1, A2, A23, Lm44;

reconsider j = j, i = i as Element of NAT by INT_1:3;

set x = ((j - 1) * ((len s1) - 1)) + i;

reconsider x = ((j - 1) * ((len s1) - 1)) + i as set ;

[x,y] in p by A24;

hence y in rng p by XTUPLE_0:def 13; :: thesis: verum

end;reconsider l9 = ((len s1) - 1) * ((len s2) - 1) as Element of NAT by A3, INT_1:3;

let y be object ; :: thesis: ( y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) implies y in rng p )

assume A19: y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ; :: thesis: y in rng p

then reconsider k = y as Element of NAT ;

A20: y in Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A19, FINSEQ_1:def 3;

then A21: 1 <= k by FINSEQ_1:1;

A22: k <= ((len s1) - 1) * ((len s2) - 1) by A17, A18, A20, FINSEQ_1:1;

0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;

then k <= l9 + 1 by A22, XXREAL_0:2;

then A23: k in Seg (l9 + 1) by A21;

k <> l9 + 1 by A22, NAT_1:13;

then consider i, j being Nat such that

A24: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) by A1, A2, A23, Lm44;

reconsider j = j, i = i as Element of NAT by INT_1:3;

set x = ((j - 1) * ((len s1) - 1)) + i;

reconsider x = ((j - 1) * ((len s1) - 1)) + i as set ;

[x,y] in p by A24;

hence y in rng p by XTUPLE_0:def 13; :: thesis: verum

A26: dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) = Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by FINSEQ_1:def 3;

now :: thesis: for x being object st x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) holds

x in dom p

then A32:
dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) c= dom p
;x in dom p

set l9 = ((len s1) - 1) * ((len s2) - 1);

reconsider l9 = ((len s1) - 1) * ((len s2) - 1) as Element of NAT by A3, INT_1:3;

let x be object ; :: thesis: ( x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) implies x in dom p )

assume A27: x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ; :: thesis: x in dom p

then reconsider k = x as Element of NAT ;

A28: k <= ((len s1) - 1) * ((len s2) - 1) by A17, A18, A26, A27, FINSEQ_1:1;

0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;

then A29: k <= l9 + 1 by A28, XXREAL_0:2;

1 <= k by A26, A27, FINSEQ_1:1;

then A30: k in Seg (l9 + 1) by A29;

k <> l9 + 1 by A28, NAT_1:13;

then consider j, i being Nat such that

A31: ( k = ((j - 1) * ((len s1) - 1)) + i & 1 <= j & j <= (len s2) - 1 & 1 <= i & i <= (len s1) - 1 ) by A1, A2, A30, Lm44;

reconsider j = j, i = i as Element of NAT by INT_1:3;

set y = ((i - 1) * ((len s2) - 1)) + j;

reconsider y = ((i - 1) * ((len s2) - 1)) + j as set ;

[x,y] in p by A31;

hence x in dom p by XTUPLE_0:def 12; :: thesis: verum

end;reconsider l9 = ((len s1) - 1) * ((len s2) - 1) as Element of NAT by A3, INT_1:3;

let x be object ; :: thesis: ( x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) implies x in dom p )

assume A27: x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ; :: thesis: x in dom p

then reconsider k = x as Element of NAT ;

A28: k <= ((len s1) - 1) * ((len s2) - 1) by A17, A18, A26, A27, FINSEQ_1:1;

0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;

then A29: k <= l9 + 1 by A28, XXREAL_0:2;

1 <= k by A26, A27, FINSEQ_1:1;

then A30: k in Seg (l9 + 1) by A29;

k <> l9 + 1 by A28, NAT_1:13;

then consider j, i being Nat such that

A31: ( k = ((j - 1) * ((len s1) - 1)) + i & 1 <= j & j <= (len s2) - 1 & 1 <= i & i <= (len s1) - 1 ) by A1, A2, A30, Lm44;

reconsider j = j, i = i as Element of NAT by INT_1:3;

set y = ((i - 1) * ((len s2) - 1)) + j;

reconsider y = ((i - 1) * ((len s2) - 1)) + j as set ;

[x,y] in p by A31;

hence x in dom p by XTUPLE_0:def 12; :: thesis: verum

now :: thesis: for y being object st y in rng p holds

y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

then
rng p c= dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))
;y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

let y be object ; :: thesis: ( y in rng p implies y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) )

set k = y;

assume y in rng p ; :: thesis: y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

then consider x being object such that

A33: [x,y] in p by XTUPLE_0:def 13;

consider i, j being Element of NAT such that

A34: [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] = [x,y] and

A35: ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) by A33;

A36: y = ((i - 1) * ((len s2) - 1)) + j by A34, XTUPLE_0:1;

reconsider k = y as Integer by A34, XTUPLE_0:1;

1 <= k by A2, A35, A36, Lm46;

then reconsider k = k as Element of NAT by INT_1:3;

( 1 <= k & k <= len (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ) by A2, A17, A18, A35, A36, Lm46;

hence y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A26; :: thesis: verum

end;set k = y;

assume y in rng p ; :: thesis: y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

then consider x being object such that

A33: [x,y] in p by XTUPLE_0:def 13;

consider i, j being Element of NAT such that

A34: [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] = [x,y] and

A35: ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) by A33;

A36: y = ((i - 1) * ((len s2) - 1)) + j by A34, XTUPLE_0:1;

reconsider k = y as Integer by A34, XTUPLE_0:1;

1 <= k by A2, A35, A36, Lm46;

then reconsider k = k as Element of NAT by INT_1:3;

( 1 <= k & k <= len (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ) by A2, A17, A18, A35, A36, Lm46;

hence y in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A26; :: thesis: verum

then A37: rng p = dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A25, XBOOLE_0:def 10;

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

x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

then
dom p c= dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))
;x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

let x be object ; :: thesis: ( x in dom p implies x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) )

set k = x;

assume x in dom p ; :: thesis: x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

then consider y being object such that

A38: [x,y] in p by XTUPLE_0:def 12;

consider i, j being Element of NAT such that

A39: [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] = [x,y] and

A40: ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) by A38;

A41: x = ((j - 1) * ((len s1) - 1)) + i by A39, XTUPLE_0:1;

reconsider k = x as Integer by A39, XTUPLE_0:1;

1 <= k by A1, A40, A41, Lm46;

then reconsider k = k as Element of NAT by INT_1:3;

( 1 <= k & k <= len (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ) by A1, A17, A18, A40, A41, Lm46;

hence x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A26; :: thesis: verum

end;set k = x;

assume x in dom p ; :: thesis: x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))

then consider y being object such that

A38: [x,y] in p by XTUPLE_0:def 12;

consider i, j being Element of NAT such that

A39: [(((j - 1) * ((len s1) - 1)) + i),(((i - 1) * ((len s2) - 1)) + j)] = [x,y] and

A40: ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) by A38;

A41: x = ((j - 1) * ((len s1) - 1)) + i by A39, XTUPLE_0:1;

reconsider k = x as Integer by A39, XTUPLE_0:1;

1 <= k by A1, A40, A41, Lm46;

then reconsider k = k as Element of NAT by INT_1:3;

( 1 <= k & k <= len (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ) by A1, A17, A18, A40, A41, Lm46;

hence x in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A26; :: thesis: verum

then A42: dom p = dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by A32, XBOOLE_0:def 10;

then reconsider p = p as Function of (dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))),(dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A37, FUNCT_2:1;

A43: p is onto by A37;

now :: thesis: for x1, x2 being object st x1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & x2 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & p . x1 = p . x2 holds

x1 = x2

then
p is one-to-one
by FUNCT_2:56;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & x2 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & p . x1 = p . x2 implies x1 = x2 )

assume that

A44: x1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) and

A45: x2 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ; :: thesis: ( p . x1 = p . x2 implies x1 = x2 )

assume A46: p . x1 = p . x2 ; :: thesis: x1 = x2

[x1,(p . x1)] in p by A32, A44, FUNCT_1:def 2;

then consider i1, j1 being Element of NAT such that

A47: [(((j1 - 1) * ((len s1) - 1)) + i1),(((i1 - 1) * ((len s2) - 1)) + j1)] = [x1,(p . x1)] and

A48: 1 <= i1 and

i1 <= (len s1) - 1 and

A49: ( 1 <= j1 & j1 <= (len s2) - 1 ) ;

[x2,(p . x2)] in p by A32, A45, FUNCT_1:def 2;

then consider i2, j2 being Element of NAT such that

A50: [(((j2 - 1) * ((len s1) - 1)) + i2),(((i2 - 1) * ((len s2) - 1)) + j2)] = [x2,(p . x2)] and

A51: 1 <= i2 and

i2 <= (len s1) - 1 and

A52: ( 1 <= j2 & j2 <= (len s2) - 1 ) ;

A53: ((i2 - 1) * ((len s2) - 1)) + j2 = p . x2 by A50, XTUPLE_0:1;

A54: ((i1 - 1) * ((len s2) - 1)) + j1 = p . x1 by A47, XTUPLE_0:1;

then i1 = i2 by A2, A46, A48, A49, A51, A52, A53, Lm45;

hence x1 = x2 by A46, A47, A50, A54, A53, XTUPLE_0:1; :: thesis: verum

end;assume that

A44: x1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) and

A45: x2 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) ; :: thesis: ( p . x1 = p . x2 implies x1 = x2 )

assume A46: p . x1 = p . x2 ; :: thesis: x1 = x2

[x1,(p . x1)] in p by A32, A44, FUNCT_1:def 2;

then consider i1, j1 being Element of NAT such that

A47: [(((j1 - 1) * ((len s1) - 1)) + i1),(((i1 - 1) * ((len s2) - 1)) + j1)] = [x1,(p . x1)] and

A48: 1 <= i1 and

i1 <= (len s1) - 1 and

A49: ( 1 <= j1 & j1 <= (len s2) - 1 ) ;

[x2,(p . x2)] in p by A32, A45, FUNCT_1:def 2;

then consider i2, j2 being Element of NAT such that

A50: [(((j2 - 1) * ((len s1) - 1)) + i2),(((i2 - 1) * ((len s2) - 1)) + j2)] = [x2,(p . x2)] and

A51: 1 <= i2 and

i2 <= (len s1) - 1 and

A52: ( 1 <= j2 & j2 <= (len s2) - 1 ) ;

A53: ((i2 - 1) * ((len s2) - 1)) + j2 = p . x2 by A50, XTUPLE_0:1;

A54: ((i1 - 1) * ((len s2) - 1)) + j1 = p . x1 by A47, XTUPLE_0:1;

then i1 = i2 by A2, A46, A48, A49, A51, A52, A53, Lm45;

hence x1 = x2 by A46, A47, A50, A54, A53, XTUPLE_0:1; :: thesis: verum

then reconsider p = p as Permutation of (dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A43;

take p = p; :: thesis: the_series_of_quotients_of (the_schreier_series_of (s1,s2)), the_series_of_quotients_of (the_schreier_series_of (s2,s1)) are_equivalent_under p,O

A55: len (the_schreier_series_of (s2,s1)) > 1 by A1, A2, A7, Def35;

then A56: (len (the_series_of_quotients_of (the_schreier_series_of (s2,s1)))) + 1 = len (the_schreier_series_of (s2,s1)) by Def33;

now :: thesis: for H1, H2 being GroupWithOperators of O

for k1, k2 being Nat st k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & k2 = (p ") . k1 & H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 holds

H1,H2 are_isomorphic

hence
the_series_of_quotients_of (the_schreier_series_of (s1,s2)), the_series_of_quotients_of (the_schreier_series_of (s2,s1)) are_equivalent_under p,O
by A4, A5, A17, A56; :: thesis: verumfor k1, k2 being Nat st k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & k2 = (p ") . k1 & H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 holds

H1,H2 are_isomorphic

(len s2) + 1 > 1 + 1
by A2, XREAL_1:6;

then len s2 >= 2 by NAT_1:13;

then A57: (len s2) - 1 >= 2 - 1 by XREAL_1:9;

set l = (((len s1) - 1) * ((len s2) - 1)) + 1;

let H1, H2 be GroupWithOperators of O; :: thesis: for k1, k2 being Nat st k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & k2 = (p ") . k1 & H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 holds

H1,H2 are_isomorphic

let k1, k2 be Nat; :: thesis: ( k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & k2 = (p ") . k1 & H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 implies H1,H2 are_isomorphic )

assume that

A58: k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) and

A59: k2 = (p ") . k1 ; :: thesis: ( H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 implies H1,H2 are_isomorphic )

(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 A57, INT_1:3;

assume that

A60: H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 and

A61: H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 ; :: thesis: H1,H2 are_isomorphic

A62: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;

then A63: Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) c= Seg l by A17, A62, FINSEQ_1:5;

A64: k1 in Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A58, FINSEQ_1:def 3;

then k1 <= len (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by FINSEQ_1:1;

then k1 <> (((len s1) - 1) * ((len s2) - 1)) + 1 by A17, A62, NAT_1:13;

then consider i, j being Nat such that

A65: k1 = ((i - 1) * ((len s2) - 1)) + j and

A66: 1 <= i and

A67: i <= (len s1) - 1 and

A68: 1 <= j and

A69: j <= (len s2) - 1 by A1, A2, A64, A63, Lm44;

reconsider H = s1 . i, K = s2 . j, H9 = s1 . (i + 1), K9 = s2 . (j + 1) as strict StableSubgroup of G by A66, A67, A68, A69, Th111;

A70: (p ") . k1 in rng (p ") by A58, FUNCT_2:4;

p . k2 = k1 by A25, A58, A59, FUNCT_1:35;

then [k2,k1] in p by A42, A59, A70, FUNCT_1:1;

then consider i9, j9 being Element of NAT such that

A71: [k2,k1] = [(((j9 - 1) * ((len s1) - 1)) + i9),(((i9 - 1) * ((len s2) - 1)) + j9)] and

A72: 1 <= i9 and

i9 <= (len s1) - 1 and

A73: ( 1 <= j9 & j9 <= (len s2) - 1 ) ;

set JK = K9 "\/" (K /\ H9);

A74: ((i - 1) * ((len s2) - 1)) + j = ((i9 - 1) * ((len s2) - 1)) + j9 by A65, A71, XTUPLE_0:1;

then A75: i = i9 by A2, A66, A68, A69, A72, A73, Lm45;

then rng (p ") c= Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by FINSEQ_1:def 3;

then (p ") . k1 in Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A70;

then A95: k2 in dom (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) by A4, A5, A17, A56, A59, FINSEQ_1:def 3;

A96: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K ) by A66, A67, A68, A69, Th112;

then reconsider JK = K9 "\/" (K /\ H9) as normal StableSubgroup of K9 "\/" (K /\ H) by Th92;

k2 = ((j - 1) * ((len s1) - 1)) + i by A71, A74, A75, XTUPLE_0:1;

then (the_schreier_series_of (s2,s1)) . k2 = K9 "\/" (K /\ H) by A1, A2, A66, A67, A68, A69, Def35;

then A97: H2 = (K9 "\/" (K /\ H)) ./. JK by A55, A61, A95, A76, Def33;

set JH = H9 "\/" (H /\ K9);

(the_schreier_series_of (s1,s2)) . k1 = H9 "\/" (H /\ K) by A1, A2, A65, A66, A67, A68, A69, Def35;

then H1 = (H9 "\/" (H /\ K)) ./. JH by A16, A58, A60, A98, Def33;

hence H1,H2 are_isomorphic by A96, A97, Th93; :: thesis: verum

end;then len s2 >= 2 by NAT_1:13;

then A57: (len s2) - 1 >= 2 - 1 by XREAL_1:9;

set l = (((len s1) - 1) * ((len s2) - 1)) + 1;

let H1, H2 be GroupWithOperators of O; :: thesis: for k1, k2 being Nat st k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & k2 = (p ") . k1 & H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 holds

H1,H2 are_isomorphic

let k1, k2 be Nat; :: thesis: ( k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) & k2 = (p ") . k1 & H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 implies H1,H2 are_isomorphic )

assume that

A58: k1 in dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) and

A59: k2 = (p ") . k1 ; :: thesis: ( H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 & H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 implies H1,H2 are_isomorphic )

(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 A57, INT_1:3;

assume that

A60: H1 = (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) . k1 and

A61: H2 = (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) . k2 ; :: thesis: H1,H2 are_isomorphic

A62: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def35;

0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;

then A63: Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) c= Seg l by A17, A62, FINSEQ_1:5;

A64: k1 in Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A58, FINSEQ_1:def 3;

then k1 <= len (the_series_of_quotients_of (the_schreier_series_of (s1,s2))) by FINSEQ_1:1;

then k1 <> (((len s1) - 1) * ((len s2) - 1)) + 1 by A17, A62, NAT_1:13;

then consider i, j being Nat such that

A65: k1 = ((i - 1) * ((len s2) - 1)) + j and

A66: 1 <= i and

A67: i <= (len s1) - 1 and

A68: 1 <= j and

A69: j <= (len s2) - 1 by A1, A2, A64, A63, Lm44;

reconsider H = s1 . i, K = s2 . j, H9 = s1 . (i + 1), K9 = s2 . (j + 1) as strict StableSubgroup of G by A66, A67, A68, A69, Th111;

A70: (p ") . k1 in rng (p ") by A58, FUNCT_2:4;

p . k2 = k1 by A25, A58, A59, FUNCT_1:35;

then [k2,k1] in p by A42, A59, A70, FUNCT_1:1;

then consider i9, j9 being Element of NAT such that

A71: [k2,k1] = [(((j9 - 1) * ((len s1) - 1)) + i9),(((i9 - 1) * ((len s2) - 1)) + j9)] and

A72: 1 <= i9 and

i9 <= (len s1) - 1 and

A73: ( 1 <= j9 & j9 <= (len s2) - 1 ) ;

set JK = K9 "\/" (K /\ H9);

A74: ((i - 1) * ((len s2) - 1)) + j = ((i9 - 1) * ((len s2) - 1)) + j9 by A65, A71, XTUPLE_0:1;

then A75: i = i9 by A2, A66, A68, A69, A72, A73, Lm45;

A76: now :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)end;

rng (p ") c= dom (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))
;per cases
( i = (len s1) - 1 or i <> (len s1) - 1 )
;

end;

suppose A77:
i = (len s1) - 1
; :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)

end;

per cases
( j <> (len s2) - 1 or j = (len s2) - 1 )
;

end;

suppose A78:
j <> (len s2) - 1
; :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)

set j9 = j + 1;

A79: 0 + (j + 1) <= 1 + (j + 1) by XREAL_1:6;

set i9 = 1;

set H3 = s1 . 1;

H9 = (1). G by A77, Def28;

then A80: K9 "\/" (K /\ H9) = K9 "\/" ((1). G) by Th21

.= K9 by Th33 ;

set H2 = s2 . (j + 1);

set H1 = s2 . ((j + 1) + 1);

1 + 1 <= j + 1 by A68, XREAL_1:6;

then A81: 1 <= j + 1 by XXREAL_0:2;

j < (len s2) - 1 by A69, A78, XXREAL_0:1;

then A82: j + 1 <= (len s2) - 1 by INT_1:7;

then A83: (j + 1) + 1 <= ((len s2) - 1) + 1 by XREAL_1:6;

then j + 1 <= len s2 by A79, XXREAL_0:2;

then j + 1 in Seg (len s2) by A81;

then A84: j + 1 in dom s2 by FINSEQ_1:def 3;

(len s1) - 1 > 1 - 1 by A1, XREAL_1:9;

then A85: (len s1) - 1 >= 0 + 1 by INT_1:7;

then reconsider H1 = s2 . ((j + 1) + 1), H2 = s2 . (j + 1), H3 = s1 . 1 as strict StableSubgroup of G by A82, A81, Th111;

A86: H3 = (Omega). G by Def28;

then A88: the carrier of H2 = the carrier of H2 /\ the carrier of ((Omega). G) by XBOOLE_1:28;

k2 + 1 = (((j + 1) - 1) * ((len s1) - 1)) + 1 by A71, A74, A75, A77, XTUPLE_0:1;

then (the_schreier_series_of (s2,s1)) . (k2 + 1) = H1 "\/" (H2 /\ H3) by A1, A2, A82, A81, A85, Def35;

then A89: (the_schreier_series_of (s2,s1)) . (k2 + 1) = H1 "\/" H2 by A86, A88, Th18;

1 <= (j + 1) + 1 by A81, A79, XXREAL_0:2;

then (j + 1) + 1 in Seg (len s2) by A83;

then (j + 1) + 1 in dom s2 by FINSEQ_1:def 3;

then H1 is normal StableSubgroup of H2 by A84, Def28;

hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A89, A80, Th36; :: thesis: verum

end;A79: 0 + (j + 1) <= 1 + (j + 1) by XREAL_1:6;

set i9 = 1;

set H3 = s1 . 1;

H9 = (1). G by A77, Def28;

then A80: K9 "\/" (K /\ H9) = K9 "\/" ((1). G) by Th21

.= K9 by Th33 ;

set H2 = s2 . (j + 1);

set H1 = s2 . ((j + 1) + 1);

1 + 1 <= j + 1 by A68, XREAL_1:6;

then A81: 1 <= j + 1 by XXREAL_0:2;

j < (len s2) - 1 by A69, A78, XXREAL_0:1;

then A82: j + 1 <= (len s2) - 1 by INT_1:7;

then A83: (j + 1) + 1 <= ((len s2) - 1) + 1 by XREAL_1:6;

then j + 1 <= len s2 by A79, XXREAL_0:2;

then j + 1 in Seg (len s2) by A81;

then A84: j + 1 in dom s2 by FINSEQ_1:def 3;

(len s1) - 1 > 1 - 1 by A1, XREAL_1:9;

then A85: (len s1) - 1 >= 0 + 1 by INT_1:7;

then reconsider H1 = s2 . ((j + 1) + 1), H2 = s2 . (j + 1), H3 = s1 . 1 as strict StableSubgroup of G by A82, A81, Th111;

A86: H3 = (Omega). G by Def28;

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 A87: 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 A87; :: thesis: verum

end;H2 is Subgroup of G by Def7;

then A87: 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 A87; :: thesis: verum

then A88: the carrier of H2 = the carrier of H2 /\ the carrier of ((Omega). G) by XBOOLE_1:28;

k2 + 1 = (((j + 1) - 1) * ((len s1) - 1)) + 1 by A71, A74, A75, A77, XTUPLE_0:1;

then (the_schreier_series_of (s2,s1)) . (k2 + 1) = H1 "\/" (H2 /\ H3) by A1, A2, A82, A81, A85, Def35;

then A89: (the_schreier_series_of (s2,s1)) . (k2 + 1) = H1 "\/" H2 by A86, A88, Th18;

1 <= (j + 1) + 1 by A81, A79, XXREAL_0:2;

then (j + 1) + 1 in Seg (len s2) by A83;

then (j + 1) + 1 in dom s2 by FINSEQ_1:def 3;

then H1 is normal StableSubgroup of H2 by A84, Def28;

hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A89, A80, Th36; :: thesis: verum

suppose A90:
j = (len s2) - 1
; :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)

then A91:
K9 = (1). G
by Def28;

H9 = (1). G by A77, Def28;

then A92: K9 "\/" (K /\ H9) = ((1). G) "\/" ((1). G) by A91, Th21

.= (1). G by Th33 ;

k2 = ((len s1) - 1) * ((len s2) - 1) by A71, A74, A75, A77, A90, XTUPLE_0:1;

hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A1, A2, A92, Def35; :: thesis: verum

end;H9 = (1). G by A77, Def28;

then A92: K9 "\/" (K /\ H9) = ((1). G) "\/" ((1). G) by A91, Th21

.= (1). G by Th33 ;

k2 = ((len s1) - 1) * ((len s2) - 1) by A71, A74, A75, A77, A90, XTUPLE_0:1;

hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A1, A2, A92, Def35; :: thesis: verum

suppose
i <> (len s1) - 1
; :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)

then
i < (len s1) - 1
by A67, XXREAL_0:1;

then A93: i + 1 <= (len s1) - 1 by INT_1:7;

set i9 = i + 1;

set k29 = k2 + 1;

1 + 1 <= i + 1 by A66, XREAL_1:6;

then A94: 1 <= i + 1 by XXREAL_0:2;

k2 + 1 = (((j - 1) * ((len s1) - 1)) + i) + 1 by A71, A74, A75, XTUPLE_0:1;

then k2 + 1 = ((j - 1) * ((len s1) - 1)) + (i + 1) ;

hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A1, A2, A68, A69, A93, A94, Def35; :: thesis: verum

end;then A93: i + 1 <= (len s1) - 1 by INT_1:7;

set i9 = i + 1;

set k29 = k2 + 1;

1 + 1 <= i + 1 by A66, XREAL_1:6;

then A94: 1 <= i + 1 by XXREAL_0:2;

k2 + 1 = (((j - 1) * ((len s1) - 1)) + i) + 1 by A71, A74, A75, XTUPLE_0:1;

then k2 + 1 = ((j - 1) * ((len s1) - 1)) + (i + 1) ;

hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A1, A2, A68, A69, A93, A94, Def35; :: thesis: verum

then rng (p ") c= Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by FINSEQ_1:def 3;

then (p ") . k1 in Seg (len (the_series_of_quotients_of (the_schreier_series_of (s1,s2)))) by A70;

then A95: k2 in dom (the_series_of_quotients_of (the_schreier_series_of (s2,s1))) by A4, A5, A17, A56, A59, FINSEQ_1:def 3;

A96: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K ) by A66, A67, A68, A69, Th112;

then reconsider JK = K9 "\/" (K /\ H9) as normal StableSubgroup of K9 "\/" (K /\ H) by Th92;

k2 = ((j - 1) * ((len s1) - 1)) + i by A71, A74, A75, XTUPLE_0:1;

then (the_schreier_series_of (s2,s1)) . k2 = K9 "\/" (K /\ H) by A1, A2, A66, A67, A68, A69, Def35;

then A97: H2 = (K9 "\/" (K /\ H)) ./. JK by A55, A61, A95, A76, Def33;

set JH = H9 "\/" (H /\ K9);

A98: now :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)end;

reconsider JH = H9 "\/" (H /\ K9) as normal StableSubgroup of H9 "\/" (H /\ K) by A96, Th92;per cases
( j = (len s2) - 1 or j <> (len s2) - 1 )
;

end;

suppose A99:
j = (len s2) - 1
; :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)

end;

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

end;

suppose A100:
i <> (len s1) - 1
; :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)

set j9 = 1;

set H3 = s2 . 1;

set i9 = i + 1;

A101: 0 + (i + 1) <= 1 + (i + 1) by XREAL_1:6;

set H2 = s1 . (i + 1);

set H1 = s1 . ((i + 1) + 1);

1 + 1 <= i + 1 by A66, XREAL_1:6;

then A102: 1 <= i + 1 by XXREAL_0:2;

i < (len s1) - 1 by A67, A100, XXREAL_0:1;

then A103: i + 1 <= (len s1) - 1 by INT_1:7;

then A104: (i + 1) + 1 <= ((len s1) - 1) + 1 by XREAL_1:6;

then i + 1 <= len s1 by A101, XXREAL_0:2;

then i + 1 in Seg (len s1) by A102;

then A105: i + 1 in dom s1 by FINSEQ_1:def 3;

(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;

then A106: (len s2) - 1 >= 0 + 1 by INT_1:7;

then reconsider H1 = s1 . ((i + 1) + 1), H2 = s1 . (i + 1), H3 = s2 . 1 as strict StableSubgroup of G by A103, A102, Th111;

A107: H3 = (Omega). G by Def28;

then A109: the carrier of H2 = the carrier of H2 /\ the carrier of ((Omega). G) by XBOOLE_1:28;

k1 + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by A65, A99;

then (the_schreier_series_of (s1,s2)) . (k1 + 1) = H1 "\/" (H2 /\ H3) by A1, A2, A103, A102, A106, Def35;

then A110: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H1 "\/" H2 by A107, A109, Th18;

1 <= (i + 1) + 1 by A102, A101, XXREAL_0:2;

then (i + 1) + 1 in Seg (len s1) by A104;

then (i + 1) + 1 in dom s1 by FINSEQ_1:def 3;

then A111: H1 is normal StableSubgroup of H2 by A105, Def28;

H9 "\/" (H /\ K9) = H9 "\/" (H /\ ((1). G)) by A99, Def28

.= H9 "\/" ((1). G) by Th21

.= H9 by Th33 ;

hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by A110, A111, Th36; :: thesis: verum

end;set H3 = s2 . 1;

set i9 = i + 1;

A101: 0 + (i + 1) <= 1 + (i + 1) by XREAL_1:6;

set H2 = s1 . (i + 1);

set H1 = s1 . ((i + 1) + 1);

1 + 1 <= i + 1 by A66, XREAL_1:6;

then A102: 1 <= i + 1 by XXREAL_0:2;

i < (len s1) - 1 by A67, A100, XXREAL_0:1;

then A103: i + 1 <= (len s1) - 1 by INT_1:7;

then A104: (i + 1) + 1 <= ((len s1) - 1) + 1 by XREAL_1:6;

then i + 1 <= len s1 by A101, XXREAL_0:2;

then i + 1 in Seg (len s1) by A102;

then A105: i + 1 in dom s1 by FINSEQ_1:def 3;

(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;

then A106: (len s2) - 1 >= 0 + 1 by INT_1:7;

then reconsider H1 = s1 . ((i + 1) + 1), H2 = s1 . (i + 1), H3 = s2 . 1 as strict StableSubgroup of G by A103, A102, Th111;

A107: H3 = (Omega). G by Def28;

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 A108: 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 A108; :: thesis: verum

end;H2 is Subgroup of G by Def7;

then A108: 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 A108; :: thesis: verum

then A109: the carrier of H2 = the carrier of H2 /\ the carrier of ((Omega). G) by XBOOLE_1:28;

k1 + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by A65, A99;

then (the_schreier_series_of (s1,s2)) . (k1 + 1) = H1 "\/" (H2 /\ H3) by A1, A2, A103, A102, A106, Def35;

then A110: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H1 "\/" H2 by A107, A109, Th18;

1 <= (i + 1) + 1 by A102, A101, XXREAL_0:2;

then (i + 1) + 1 in Seg (len s1) by A104;

then (i + 1) + 1 in dom s1 by FINSEQ_1:def 3;

then A111: H1 is normal StableSubgroup of H2 by A105, Def28;

H9 "\/" (H /\ K9) = H9 "\/" (H /\ ((1). G)) by A99, Def28

.= H9 "\/" ((1). G) by Th21

.= H9 by Th33 ;

hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by A110, A111, Th36; :: thesis: verum

suppose A112:
i = (len s1) - 1
; :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)

then A113:
k1 = ((len s1) - 1) * ((len s2) - 1)
by A65, A99;

A114: K9 = (1). G by A99, Def28;

H9 = (1). G by A112, Def28;

then H9 "\/" (H /\ K9) = ((1). G) "\/" ((1). G) by A114, Th21

.= (1). G by Th33 ;

hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by A1, A2, A113, Def35; :: thesis: verum

end;A114: K9 = (1). G by A99, Def28;

H9 = (1). G by A112, Def28;

then H9 "\/" (H /\ K9) = ((1). G) "\/" ((1). G) by A114, Th21

.= (1). G by Th33 ;

hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by A1, A2, A113, Def35; :: thesis: verum

suppose
j <> (len s2) - 1
; :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)

then
j < (len s2) - 1
by A69, XXREAL_0:1;

then A115: j + 1 <= (len s2) - 1 by INT_1:7;

set j9 = j + 1;

set k19 = k1 + 1;

1 + 1 <= j + 1 by A68, XREAL_1:6;

then A116: 1 <= j + 1 by XXREAL_0:2;

k1 + 1 = ((i - 1) * ((len s2) - 1)) + (j + 1) by A65;

hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by A1, A2, A66, A67, A115, A116, Def35; :: thesis: verum

end;then A115: j + 1 <= (len s2) - 1 by INT_1:7;

set j9 = j + 1;

set k19 = k1 + 1;

1 + 1 <= j + 1 by A68, XREAL_1:6;

then A116: 1 <= j + 1 by XXREAL_0:2;

k1 + 1 = ((i - 1) * ((len s2) - 1)) + (j + 1) by A65;

hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by A1, A2, A66, A67, A115, A116, Def35; :: thesis: verum

(the_schreier_series_of (s1,s2)) . k1 = H9 "\/" (H /\ K) by A1, A2, A65, A66, A67, A68, A69, Def35;

then H1 = (H9 "\/" (H /\ K)) ./. JH by A16, A58, A60, A98, Def33;

hence H1,H2 are_isomorphic by A96, A97, Th93; :: thesis: verum

hence the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) by A6, A8, Th108; :: thesis: verum