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:
set s21 = the_schreier_series_of (s2,s1);
A3: ( (len s1) - 1 > 1 - 1 & (len s2) - 1 > 1 - 1 ) by ;
set s12 = the_schreier_series_of (s1,s2);
A4: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by ;
A5: len (the_schreier_series_of (s2,s1)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by ;
then A6: not the_schreier_series_of (s2,s1) is empty by A3;
((len s1) - 1) * ((len s2) - 1) > 0 * ((len s2) - 1) by ;
then A7: (((len s1) - 1) * ((len s2) - 1)) + 1 > 0 + 1 by XREAL_1:6;
A8: now :: thesis: ex p being Permutation of (dom ()) 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
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 ) } ;
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]
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;
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;
set X = dom ();
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
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 ;
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 ;
then j1 = j2 by A1, A11, A14, A12, Lm45;
hence y1 = y2 by ; :: thesis: verum
end;
then reconsider p = p as Function by FUNCT_1:def 1;
A16: len (the_schreier_series_of (s1,s2)) > 1 by A1, A2, A7, Def35;
then A17: (len ()) + 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 ;
now :: thesis: for y being object st y in dom () holds
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 ;
let y be object ; :: thesis: ( y in dom () implies y in rng p )
assume A19: y in dom () ; :: thesis: y in rng p
then reconsider k = y as Element of NAT ;
A20: y in Seg (len ()) by ;
then A21: 1 <= k by FINSEQ_1:1;
A22: k <= ((len s1) - 1) * ((len s2) - 1) by ;
0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;
then k <= l9 + 1 by ;
then A23: k in Seg (l9 + 1) by A21;
k <> l9 + 1 by ;
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;
then A25: dom () c= rng p ;
A26: dom () = Seg (len ()) by FINSEQ_1:def 3;
now :: thesis: for x being object st x in dom () holds
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 ;
let x be object ; :: thesis: ( x in dom () implies x in dom p )
assume A27: x in dom () ; :: thesis: x in dom p
then reconsider k = x as Element of NAT ;
A28: k <= ((len s1) - 1) * ((len s2) - 1) by ;
0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;
then A29: k <= l9 + 1 by ;
1 <= k by ;
then A30: k in Seg (l9 + 1) by A29;
k <> l9 + 1 by ;
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;
then A32: dom () c= dom p ;
now :: thesis: for y being object st y in rng p holds
y in dom ()
let y be object ; :: thesis: ( y in rng p implies y in dom () )
set k = y;
assume y in rng p ; :: thesis: y in dom ()
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 ;
reconsider k = y as Integer by ;
1 <= k by A2, A35, A36, Lm46;
then reconsider k = k as Element of NAT by INT_1:3;
( 1 <= k & k <= len () ) by A2, A17, A18, A35, A36, Lm46;
hence y in dom () by A26; :: thesis: verum
end;
then rng p c= dom () ;
then A37: rng p = dom () by ;
now :: thesis: for x being object st x in dom p holds
x in dom ()
let x be object ; :: thesis: ( x in dom p implies x in dom () )
set k = x;
assume x in dom p ; :: thesis: x in dom ()
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 ;
reconsider k = x as Integer by ;
1 <= k by A1, A40, A41, Lm46;
then reconsider k = k as Element of NAT by INT_1:3;
( 1 <= k & k <= len () ) by A1, A17, A18, A40, A41, Lm46;
hence x in dom () by A26; :: thesis: verum
end;
then dom p c= dom () ;
then A42: dom p = dom () by ;
then reconsider p = p as Function of (dom ()),(dom ()) by ;
A43: p is onto by A37;
now :: thesis: for x1, x2 being object st x1 in dom () & x2 in dom () & p . x1 = p . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom () & x2 in dom () & p . x1 = p . x2 implies x1 = x2 )
assume that
A44: x1 in dom () and
A45: x2 in dom () ; :: thesis: ( p . x1 = p . x2 implies x1 = x2 )
assume A46: p . x1 = p . x2 ; :: thesis: x1 = x2
[x1,(p . x1)] in p by ;
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 ;
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 ;
A54: ((i1 - 1) * ((len s2) - 1)) + j1 = p . x1 by ;
then i1 = i2 by A2, A46, A48, A49, A51, A52, A53, Lm45;
hence x1 = x2 by ; :: thesis: verum
end;
then p is one-to-one by FUNCT_2:56;
then reconsider p = p as Permutation of (dom ()) by A43;
take p = p; :: thesis:
A55: len (the_schreier_series_of (s2,s1)) > 1 by A1, A2, A7, Def35;
then A56: (len ()) + 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 () & k2 = (p ") . k1 & H1 = () . k1 & H2 = () . k2 holds
H1,H2 are_isomorphic
(len s2) + 1 > 1 + 1 by ;
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 () & k2 = (p ") . k1 & H1 = () . k1 & H2 = () . k2 holds
H1,H2 are_isomorphic

let k1, k2 be Nat; :: thesis: ( k1 in dom () & k2 = (p ") . k1 & H1 = () . k1 & H2 = () . k2 implies H1,H2 are_isomorphic )
assume that
A58: k1 in dom () and
A59: k2 = (p ") . k1 ; :: thesis: ( H1 = () . k1 & H2 = () . k2 implies H1,H2 are_isomorphic )
(len s1) + 1 > 1 + 1 by ;
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 ;
assume that
A60: H1 = () . k1 and
A61: H2 = () . k2 ; :: thesis: H1,H2 are_isomorphic
A62: len (the_schreier_series_of (s1,s2)) = (((len s1) - 1) * ((len s2) - 1)) + 1 by ;
0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:6;
then A63: Seg (len ()) c= Seg l by ;
A64: k1 in Seg (len ()) by ;
then k1 <= len () by FINSEQ_1:1;
then k1 <> (((len s1) - 1) * ((len s2) - 1)) + 1 by ;
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 ;
A70: (p ") . k1 in rng (p ") by ;
p . k2 = k1 by ;
then [k2,k1] in p by ;
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 ;
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)
per cases ( i = (len s1) - 1 or i <> (len s1) - 1 ) ;
suppose A77: i = (len s1) - 1 ; :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)
per cases ( j <> (len s2) - 1 or j = (len s2) - 1 ) ;
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 ;
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 ;
then A81: 1 <= j + 1 by XXREAL_0:2;
j < (len s2) - 1 by ;
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 ;
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 ;
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 ;
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 ()
let x be object ; :: thesis: ( x in the carrier of H2 implies x in the carrier of () )
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 ()
hence x in the carrier of () by A87; :: thesis: verum
end;
then the carrier of H2 c= the carrier of () ;
then A88: the carrier of H2 = the carrier of H2 /\ the carrier of () by XBOOLE_1:28;
k2 + 1 = (((j + 1) - 1) * ((len s1) - 1)) + 1 by ;
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 ;
1 <= (j + 1) + 1 by ;
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 ;
hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by ; :: thesis: verum
end;
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 ;
then A92: K9 "\/" (K /\ H9) = ((1). G) "\/" ((1). G) by
.= (1). G by Th33 ;
k2 = ((len s1) - 1) * ((len s2) - 1) by ;
hence (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9) by A1, A2, A92, Def35; :: thesis: verum
end;
end;
end;
suppose i <> (len s1) - 1 ; :: thesis: (the_schreier_series_of (s2,s1)) . (k2 + 1) = K9 "\/" (K /\ H9)
then i < (len s1) - 1 by ;
then A93: i + 1 <= (len s1) - 1 by INT_1:7;
set i9 = i + 1;
set k29 = k2 + 1;
1 + 1 <= i + 1 by ;
then A94: 1 <= i + 1 by XXREAL_0:2;
k2 + 1 = (((j - 1) * ((len s1) - 1)) + i) + 1 by ;
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;
end;
end;
rng (p ") c= dom () ;
then rng (p ") c= Seg (len ()) by FINSEQ_1:def 3;
then (p ") . k1 in Seg (len ()) by A70;
then A95: k2 in dom () by ;
A96: ( H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K ) by ;
then reconsider JK = K9 "\/" (K /\ H9) as normal StableSubgroup of K9 "\/" (K /\ H) by Th92;
k2 = ((j - 1) * ((len s1) - 1)) + i by ;
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 ;
set JH = H9 "\/" (H /\ K9);
A98: now :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)
per cases ( j = (len s2) - 1 or j <> (len s2) - 1 ) ;
suppose A99: j = (len s2) - 1 ; :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)
per cases ( i <> (len s1) - 1 or i = (len s1) - 1 ) ;
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 ;
then A102: 1 <= i + 1 by XXREAL_0:2;
i < (len s1) - 1 by ;
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 ;
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 ;
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 ;
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 ()
let x be object ; :: thesis: ( x in the carrier of H2 implies x in the carrier of () )
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 ()
hence x in the carrier of () by A108; :: thesis: verum
end;
then the carrier of H2 c= the carrier of () ;
then A109: the carrier of H2 = the carrier of H2 /\ the carrier of () by XBOOLE_1:28;
k1 + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by ;
then (the_schreier_series_of (s1,s2)) . (k1 + 1) = H1 "\/" (H2 /\ H3) by ;
then A110: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H1 "\/" H2 by ;
1 <= (i + 1) + 1 by ;
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 ;
H9 "\/" (H /\ K9) = H9 "\/" (H /\ ((1). G)) by
.= H9 "\/" ((1). G) by Th21
.= H9 by Th33 ;
hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by ; :: thesis: verum
end;
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 ;
A114: K9 = (1). G by ;
H9 = (1). G by ;
then H9 "\/" (H /\ K9) = ((1). G) "\/" ((1). G) by
.= (1). G by Th33 ;
hence (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9) by ; :: thesis: verum
end;
end;
end;
suppose j <> (len s2) - 1 ; :: thesis: (the_schreier_series_of (s1,s2)) . (k1 + 1) = H9 "\/" (H /\ K9)
then j < (len s2) - 1 by ;
then A115: j + 1 <= (len s2) - 1 by INT_1:7;
set j9 = j + 1;
set k19 = k1 + 1;
1 + 1 <= j + 1 by ;
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;
end;
end;
reconsider JH = H9 "\/" (H /\ K9) as normal StableSubgroup of H9 "\/" (H /\ K) by ;
(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 ;
hence H1,H2 are_isomorphic by ; :: thesis: verum
end;
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: verum
end;
not the_schreier_series_of (s1,s2) is empty by A3, A4;
hence the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) by ; :: thesis: verum