A8: now

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

let x be set ; :: thesis:
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:
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 set ;
take y = y; :: thesis:
take z = z; :: thesis:
thus x = [y,z] by A9; :: thesis:

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

let x, y1, y2 be set ; :: thesis:
assume [x,y1] in p ; :: thesis:
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, ZFMISC_1:33;
assume [x,y2] in p ; :: thesis:
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, ZFMISC_1:33;
then j1 = j2 by A1, A11, A14, A12, Lm46;
hence y1 = y2 by A10, A13, A12, A15, ZFMISC_1:33; :: thesis:

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, Def38;
then A17: (len (the_series_of_quotients_of (the_schreier_series_of s1,s2))) + 1 = len (the_schreier_series_of s1,s2) by Def36;
A18: len (the_schreier_series_of s1,s2) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def38;

now

set l9 = ((len s1) - 1) * ((len s2) - 1);
reconsider l9 = ((len s1) - 1) * ((len s2) - 1) as Element of NAT by A3, INT_1:16;
let y be set ; :: thesis:
assume A19: y in dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) ; :: thesis:
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:3;
A22: k <= ((len s1) - 1) * ((len s2) - 1) by A17, A18, A20, FINSEQ_1:3;
0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:8;
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, Lm45;
reconsider j = j, i = i as Element of NAT by INT_1:16;
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 RELAT_1:def 5; :: thesis:

end;

then A25: dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) c= rng p by TARSKI:def 3;
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

set l9 = ((len s1) - 1) * ((len s2) - 1);
reconsider l9 = ((len s1) - 1) * ((len s2) - 1) as Element of NAT by A3, INT_1:16;
let x be set ; :: thesis:
assume A27: x in dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) ; :: thesis:
then reconsider k = x as Element of NAT ;
A28: k <= ((len s1) - 1) * ((len s2) - 1) by A17, A18, A26, A27, FINSEQ_1:3;
0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:8;
then A29: k <= l9 + 1 by A28, XXREAL_0:2;
1 <= k by A26, A27, FINSEQ_1:3;
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, Lm45;
reconsider j = j, i = i as Element of NAT by INT_1:16;
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 RELAT_1:def 4; :: thesis:

end;

then A32: dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) c= dom p by TARSKI:def 3;

now

let y be set ; :: thesis:
set k = y;
assume y in rng p ; :: thesis:
then consider x being set such that
A33: [x,y] in p by RELAT_1:def 5;
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, ZFMISC_1:33;
reconsider k = y as integer number by A34, ZFMISC_1:33;
1 <= k by A2, A35, A36, Lm47;
then reconsider k = k as Element of NAT by INT_1:16;
( 1 <= k & k <= len (the_series_of_quotients_of (the_schreier_series_of s1,s2)) ) by A2, A17, A18, A35, A36, Lm47;
hence y in dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) by A26; :: thesis:

end;

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

now

let x be set ; :: thesis:
set k = x;
assume x in dom p ; :: thesis:
then consider y being set such that
A38: [x,y] in p by RELAT_1:def 4;
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, ZFMISC_1:33;
reconsider k = x as integer number by A39, ZFMISC_1:33;
1 <= k by A1, A40, A41, Lm47;
then reconsider k = k as Element of NAT by INT_1:16;
( 1 <= k & k <= len (the_series_of_quotients_of (the_schreier_series_of s1,s2)) ) by A1, A17, A18, A40, A41, Lm47;
hence x in dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) by A26; :: thesis:

end;

then dom p c= dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) by TARSKI:def 3;
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:3;
A43: p is onto by A37, FUNCT_2:def 3;

now

let x1, x2 be set ; :: thesis:
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:
assume A46: p . x1 = p . x2 ; :: thesis:
[x1,(p . x1)] in p by A32, A44, FUNCT_1:def 4;
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 4;
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, ZFMISC_1:33;
A54: ((i1 - 1) * ((len s2) - 1)) + j1 = p . x1 by A47, ZFMISC_1:33;
then i1 = i2 by A2, A46, A48, A49, A51, A52, A53, Lm46;
hence x1 = x2 by A46, A47, A50, A54, A53, ZFMISC_1:33; :: thesis:

end;

then p is one-to-one by FUNCT_2:77;
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:
A55: len (the_schreier_series_of s2,s1) > 1 by A1, A2, A7, Def38;
then A56: (len (the_series_of_quotients_of (the_schreier_series_of s2,s1))) + 1 = len (the_schreier_series_of s2,s1) by Def36;

now

(len s2) + 1 > 1 + 1 by A2, XREAL_1:8;
then len s2 >= 2 by NAT_1:13;
then A57: (len s2) - 1 >= 2 - 1 by XREAL_1:11;
set l = (((len s1) - 1) * ((len s2) - 1)) + 1;
let H1, H2 be GroupWithOperators of O; :: thesis:
let k1, k2 be Nat; :: thesis:
assume that
A58: k1 in dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) and
A59: k2 = (p " ) . k1 ; :: thesis:
(len s1) + 1 > 1 + 1 by A1, XREAL_1:8;
then len s1 >= 2 by NAT_1:13;
then (len s1) - 1 >= 2 - 1 by XREAL_1:11;
then reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by A57, INT_1:16;
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:
A62: len (the_schreier_series_of s1,s2) = (((len s1) - 1) * ((len s2) - 1)) + 1 by A1, A2, Def38;
0 + (((len s1) - 1) * ((len s2) - 1)) <= 1 + (((len s1) - 1) * ((len s2) - 1)) by XREAL_1:8;
then A63: Seg (len (the_series_of_quotients_of (the_schreier_series_of s1,s2))) c= Seg l by A17, A62, FINSEQ_1:7;
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:3;
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, Lm45;
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:6;
p . k2 = k1 by A25, A58, A59, FUNCT_1:57;
then [k2,k1] in p by A42, A59, A70, FUNCT_1:8;
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, ZFMISC_1:33;
then A75: i = i9 by A2, A66, A68, A69, A72, A73, Lm46;

A76: now

per cases ;

suppose A77: i = (len s1) - 1 ; :: thesis:

per cases ;

suppose A78: j <> (len s2) - 1 ; :: thesis:

set j9 = j + 1;
A79: 0 + (j + 1) <= 1 + (j + 1) by XREAL_1:8;
set i9 = 1;
set H3 = s1 . 1;
H9 = (1). G by A77, Def31;
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:8;
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:20;
then A83: (j + 1) + 1 <= ((len s2) - 1) + 1 by XREAL_1:8;
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:11;
then A85: (len s1) - 1 >= 0 + 1 by INT_1:20;
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 Def31;

now

let x be set ; :: thesis:
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:
hence x in the carrier of ((Omega). G) by A87; :: thesis:

end;

then the carrier of H2 c= the carrier of ((Omega). G) by TARSKI:def 3;
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, ZFMISC_1:33;
then (the_schreier_series_of s2,s1) . (k2 + 1) = H1 "\/" (H2 /\ H3) by A1, A2, A82, A81, A85, Def38;
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, Def31;
hence (the_schreier_series_of s2,s1) . (k2 + 1) = K9 "\/" (K /\ H9) by A89, A80, Th36; :: thesis:

end;

suppose A90: j = (len s2) - 1 ; :: thesis:

then A91: K9 = (1). G by Def31;
H9 = (1). G by A77, Def31;
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, ZFMISC_1:33;
hence (the_schreier_series_of s2,s1) . (k2 + 1) = K9 "\/" (K /\ H9) by A1, A2, A92, Def38; :: thesis:

end;

suppose i <> (len s1) - 1 ; :: thesis:

then i < (len s1) - 1 by A67, XXREAL_0:1;
then A93: i + 1 <= (len s1) - 1 by INT_1:20;
set i9 = i + 1;
set k29 = k2 + 1;
1 + 1 <= i + 1 by A66, XREAL_1:8;
then A94: 1 <= i + 1 by XXREAL_0:2;
k2 + 1 = (((j - 1) * ((len s1) - 1)) + i) + 1 by A71, A74, A75, ZFMISC_1:33;
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, Def38; :: thesis:

end;

rng (p " ) c= dom (the_series_of_quotients_of (the_schreier_series_of s1,s2)) ;
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, ZFMISC_1:33;
then (the_schreier_series_of s2,s1) . k2 = K9 "\/" (K /\ H) by A1, A2, A66, A67, A68, A69, Def38;
then A97: H2 = (K9 "\/" (K /\ H)) ./. JK by A55, A61, A95, A76, Def36;
set JH = H9 "\/" (H /\ K9);

A98: now

per cases ;

suppose A99: j = (len s2) - 1 ; :: thesis:

per cases ;

suppose A100: i <> (len s1) - 1 ; :: thesis:

set j9 = 1;
set H3 = s2 . 1;
set i9 = i + 1;
A101: 0 + (i + 1) <= 1 + (i + 1) by XREAL_1:8;
set H2 = s1 . (i + 1);
set H1 = s1 . ((i + 1) + 1);
1 + 1 <= i + 1 by A66, XREAL_1:8;
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:20;
then A104: (i + 1) + 1 <= ((len s1) - 1) + 1 by XREAL_1:8;
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:11;
then A106: (len s2) - 1 >= 0 + 1 by INT_1:20;
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 Def31;

now

let x be set ; :: thesis:
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:
hence x in the carrier of ((Omega). G) by A108; :: thesis:

end;

then the carrier of H2 c= the carrier of ((Omega). G) by TARSKI:def 3;
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, Def38;
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, Def31;
H9 "\/" (H /\ K9) = H9 "\/" (H /\ ((1). G)) by A99, Def31
.= 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:

end;

suppose A112: i = (len s1) - 1 ; :: thesis:

then A113: k1 = ((len s1) - 1) * ((len s2) - 1) by A65, A99;
A114: K9 = (1). G by A99, Def31;
H9 = (1). G by A112, Def31;
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, Def38; :: thesis:

end;

suppose j <> (len s2) - 1 ; :: thesis:

then j < (len s2) - 1 by A69, XXREAL_0:1;
then A115: j + 1 <= (len s2) - 1 by INT_1:20;
set j9 = j + 1;
set k19 = k1 + 1;
1 + 1 <= j + 1 by A68, XREAL_1:8;
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, Def38; :: thesis:

end;

reconsider JH = H9 "\/" (H /\ K9) as normal StableSubgroup of H9 "\/" (H /\ K) by A96, Th92;
(the_schreier_series_of s1,s2) . k1 = H9 "\/" (H /\ K) by A1, A2, A65, A66, A67, A68, A69, Def38;
then H1 = (H9 "\/" (H /\ K)) ./. JH by A16, A58, A60, A98, Def36;
hence H1,H2 are_isomorphic by A96, A97, Th93; :: thesis:

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, Def37; :: thesis:

end;