let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for f1, f2 being FinSequence
for i, j being Nat st f1 = the_series_of_quotients_of s1 & f2 = the_series_of_quotients_of s2 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p " ) . i ) holds
ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G
for f1, f2 being FinSequence
for i, j being Nat st f1 = the_series_of_quotients_of s1 & f2 = the_series_of_quotients_of s2 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p " ) . i ) holds
ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O
let s1, s2 be CompositionSeries of G; :: thesis: for f1, f2 being FinSequence
for i, j being Nat st f1 = the_series_of_quotients_of s1 & f2 = the_series_of_quotients_of s2 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p " ) . i ) holds
ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O
let f1, f2 be FinSequence; :: thesis: for i, j being Nat st f1 = the_series_of_quotients_of s1 & f2 = the_series_of_quotients_of s2 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p " ) . i ) holds
ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O
let i, j be Nat; :: thesis: ( f1 = the_series_of_quotients_of s1 & f2 = the_series_of_quotients_of s2 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p " ) . i ) implies ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O )
assume A1: f1 = the_series_of_quotients_of s1 ; :: thesis: ( not f2 = the_series_of_quotients_of s2 or not i in dom f1 or ex H being GroupWithOperators of O st
( H = f1 . i & not H is trivial ) or for p being Permutation of (dom f1) holds
( not f1,f2 are_equivalent_under p,O or not j = (p " ) . i ) or ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O )
assume A2: f2 = the_series_of_quotients_of s2 ; :: thesis: ( not i in dom f1 or ex H being GroupWithOperators of O st
( H = f1 . i & not H is trivial ) or for p being Permutation of (dom f1) holds
( not f1,f2 are_equivalent_under p,O or not j = (p " ) . i ) or ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O )
assume A3: i in dom f1 ; :: thesis: ( ex H being GroupWithOperators of O st
( H = f1 . i & not H is trivial ) or for p being Permutation of (dom f1) holds
( not f1,f2 are_equivalent_under p,O or not j = (p " ) . i ) or ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O )
assume for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ; :: thesis: ( for p being Permutation of (dom f1) holds
( not f1,f2 are_equivalent_under p,O or not j = (p " ) . i ) or ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O )
given p being Permutation of (dom f1) such that A5: ( f1,f2 are_equivalent_under p,O & j = (p " ) . i ) ; :: thesis: ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O
rng (p " ) c= dom f1 ;
then A6: rng (p " ) c= Seg (len f1) by FINSEQ_1:def 3;
(p " ) . i in rng (p " ) by A3, FUNCT_2:6;
then A7: (p " ) . i in Seg (len f1) by A6;
A8: len f1 = len f2 by A5, Def37;
then A9: j in dom f2 by A5, A7, FINSEQ_1:def 3;
A10: f1 . i in rng f1 by A3, FUNCT_1:12;
f2 . j in rng f2 by A9, FUNCT_1:12;
then reconsider H = f1 . i, H2 = f2 . j as strict GroupWithOperators of O by A1, A2, A10, Th102;
consider k1 being Nat such that
A13: ( len f1 = k1 + 1 & len (Del f1,i) = k1 ) by A3, FINSEQ_3:113;
consider k2 being Nat such that
A14: ( len f2 = k2 + 1 & len (Del f2,j) = k2 ) by A9, FINSEQ_3:113;
A15: ( len f1 = 0 or len f1 >= 0 + 1 ) by NAT_1:13;

per cases ( len f1 = 0 or len f1 = 1 or len f1 > 1 ) by A15, XXREAL_0:1;

suppose len f1 = 0 ; :: thesis: ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O

then A16: f1 = {} ;
consider p' being Permutation of (dom (Del f1,i));
A17: for H1, H2 being GroupWithOperators of O
for l, n being Nat st l in dom (Del f1,i) & n = (p' " ) . l & H1 = (Del f1,i) . l & H2 = (Del f2,j) . n holds
H1,H2 are_isomorphic by A16;
take p' ; :: thesis: Del f1,i, Del f2,j are_equivalent_under p',O
thus Del f1,i, Del f2,j are_equivalent_under p',O by A8, A13, A14, A17, Def37; :: thesis: verum

end;

suppose len f1 = 1 ; :: thesis: ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O

then A19: Del f1,i = {} by A13;
reconsider p' = {} as Function of (dom {} ),(rng {} ) by FUNCT_2:3;
reconsider p' = p' as Function of {} ,{} ;
p' is onto by FUNCT_2:def 3;
then reconsider p' = p' as Permutation of (dom (Del f1,i)) by A19;
take p' ; :: thesis: Del f1,i, Del f2,j are_equivalent_under p',O
for H1, H2 being GroupWithOperators of O
for l, n being Nat st l in dom (Del f1,i) & n = (p' " ) . l & H1 = (Del f1,i) . l & H2 = (Del f2,j) . n holds
H1,H2 are_isomorphic ;
hence Del f1,i, Del f2,j are_equivalent_under p',O by A8, A13, A14, Def37; :: thesis: verum

end;

suppose A20: len f1 > 1 ; :: thesis: ex p' being Permutation of (dom (Del f1,i)) st Del f1,i, Del f2,j are_equivalent_under p',O

set X = (dom f1) \ {i};
set Y = (dom f2) \ {j};
set p' = (((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j}));
(dom f1) \ {i} c= dom f1 by XBOOLE_1:36;
then A21: (dom f1) \ {i} c= Seg (len f1) by FINSEQ_1:def 3;
then A22: rng (Sgm ((dom f1) \ {i})) = (dom f1) \ {i} by FINSEQ_1:def 13;
A23: dom f1 = Seg (len f1) by FINSEQ_1:def 3
.= Seg (len f2) by A5, Def37
.= dom f2 by FINSEQ_1:def 3 ;
A24: p . j = (p * (p " )) . i by A3, A5, FUNCT_2:21
.= (id (dom f1)) . i by FUNCT_2:88
.= i by A3, FUNCT_1:35 ;
(dom f2) \ {j} c= dom f2 by XBOOLE_1:36;
then A25: (dom f2) \ {j} c= Seg (len f2) by FINSEQ_1:def 3;
(dom f2) \ {j} c= dom f2 by XBOOLE_1:36;
then A26: (dom f2) \ {j} c= Seg (len f2) by FINSEQ_1:def 3;
then A27: Sgm ((dom f2) \ {j}) is one-to-one by FINSEQ_3:99;
A28: rng (Sgm ((dom f2) \ {j})) = (dom f2) \ {j} by A26, FINSEQ_1:def 13;

A29: now

assume (dom f2) \ {j} = {} ; :: thesis: contradiction
then A30: dom f2 c= {j} by XBOOLE_1:37;
{j} c= dom f2 by A9, ZFMISC_1:37;
then A31: dom f2 = {j} by A30, XBOOLE_0:def 10;
consider k being Nat such that
A32: dom f2 = Seg k by FINSEQ_1:def 2;
k in NAT by ORDINAL1:def 13;
then k = len f2 by A32, FINSEQ_1:def 3;
then k >= 1 + 1 by A8, A20, NAT_1:13;
then Seg 2 c= Seg k by FINSEQ_1:7;
then {1,2} = {j} by A31, A32, FINSEQ_1:4, ZFMISC_1:27;
hence contradiction by ZFMISC_1:9; :: thesis: verum

end;

A33: Sgm ((dom f2) \ {j}) is Function of (dom (Sgm ((dom f2) \ {j}))),(rng (Sgm ((dom f2) \ {j}))) by FUNCT_2:3;
A34: ( (((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j})) is Permutation of (dom (Del f1,i)) & ((((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j}))) " = (((Sgm ((dom f2) \ {j})) " ) * (p " )) * (Sgm ((dom f1) \ {i})) )

proof

A35: Sgm ((dom f1) \ {i}) is one-to-one by A21, FINSEQ_3:99;
A36: dom (Del f1,i) = Seg k1 by A13, FINSEQ_1:def 3;
A37: {i} c= dom f1 by A3, ZFMISC_1:37;
A38: ((dom f1) \ {i}) \/ {i} = (dom f1) \/ {i} by XBOOLE_1:39
.= dom f1 by A37, XBOOLE_1:12 ;
card (((dom f1) \ {i}) \/ {i}) = (card ((dom f1) \ {i})) + (card {i}) by CARD_2:53, XBOOLE_1:79;
then A39: (card ((dom f1) \ {i})) + 1 = card (((dom f1) \ {i}) \/ {i}) by CARD_1:50
.= card (Seg (len f1)) by A38, FINSEQ_1:def 3
.= k1 + 1 by A13, FINSEQ_1:78 ;
A40: {j} c= dom f2 by A9, ZFMISC_1:37;
A41: ((dom f2) \ {j}) \/ {j} = (dom f2) \/ {j} by XBOOLE_1:39
.= dom f2 by A40, XBOOLE_1:12 ;
card (((dom f2) \ {j}) \/ {j}) = (card ((dom f2) \ {j})) + (card {j}) by CARD_2:53, XBOOLE_1:79;
then (card ((dom f2) \ {j})) + 1 = card (((dom f2) \ {j}) \/ {j}) by CARD_1:50
.= card (Seg (len f2)) by A41, FINSEQ_1:def 3
.= card (Seg (len f1)) by A5, Def37
.= k1 + 1 by A13, FINSEQ_1:78 ;
then A42: dom (Sgm ((dom f2) \ {j})) = Seg k1 by A25, FINSEQ_3:45;
A43: dom ((Sgm ((dom f1) \ {i})) " ) = (dom f1) \ {i} by A22, A35, FUNCT_1:55;
then dom ((Sgm ((dom f1) \ {i})) " ) c= dom f1 by XBOOLE_1:36;
then A44: dom ((Sgm ((dom f1) \ {i})) " ) c= rng p by FUNCT_2:def 3;

A45: now

let x be set ; :: thesis: ( x in dom (((Sgm ((dom f1) \ {i})) " ) * p) implies x in (dom f2) \ {j} )
assume x in dom (((Sgm ((dom f1) \ {i})) " ) * p) ; :: thesis: x in (dom f2) \ {j}
then A46: ( x in dom p & p . x in dom ((Sgm ((dom f1) \ {i})) " ) ) by FUNCT_1:21;
then ( x in dom f1 & p . x in (dom f1) \ {i} ) by A22, A35, FUNCT_1:55;
then not p . x in {i} by XBOOLE_0:def 5;
then p . x <> i by TARSKI:def 1;
then ( x in dom f2 & not x in {j} ) by A23, A24, A46, TARSKI:def 1;
hence x in (dom f2) \ {j} by XBOOLE_0:def 5; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in (dom f2) \ {j} implies x in dom (((Sgm ((dom f1) \ {i})) " ) * p) )
assume A47: x in (dom f2) \ {j} ; :: thesis: x in dom (((Sgm ((dom f1) \ {i})) " ) * p)
then ( x in dom f2 & not x in {j} ) by XBOOLE_0:def 5;
then A48: x <> j by TARSKI:def 1;
dom f1 = dom p by A3, FUNCT_2:def 1;
then A49: x in dom p by A23, A47, XBOOLE_0:def 5;
dom f1 = rng p by FUNCT_2:def 3;
then A50: p . x in dom f1 by A49, FUNCT_1:12;
p . x <> i by A9, A23, A24, A48, A49, FUNCT_2:77;
then not p . x in {i} by TARSKI:def 1;
then p . x in (dom f1) \ {i} by A50, XBOOLE_0:def 5;
hence x in dom (((Sgm ((dom f1) \ {i})) " ) * p) by A43, A49, FUNCT_1:21; :: thesis: verum

end;

then dom (((Sgm ((dom f1) \ {i})) " ) * p) = (dom f2) \ {j} by A45, TARSKI:2;
then A51: dom (((Sgm ((dom f1) \ {i})) " ) * p) = rng (Sgm ((dom f2) \ {j})) by A25, FINSEQ_1:def 13;
then rng ((((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j}))) = rng (((Sgm ((dom f1) \ {i})) " ) * p) by RELAT_1:47
.= rng ((Sgm ((dom f1) \ {i})) " ) by A44, RELAT_1:47
.= dom (Sgm ((dom f1) \ {i})) by A35, FUNCT_1:55 ;
then A52: rng ((((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by A21, A39, FINSEQ_3:45;
dom ((((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by A42, A51, RELAT_1:46;
then reconsider p' = (((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j})) as Function of (dom (Del f1,i)),(dom (Del f1,i)) by A36, A52, FUNCT_2:3;
A53: p' is onto by A36, A52, FUNCT_2:def 3;
A54: Sgm ((dom f2) \ {j}) is one-to-one by A25, FINSEQ_3:99;
(Sgm ((dom f1) \ {i})) " is one-to-one by A35;
then ((Sgm ((dom f1) \ {i})) " ) * p is one-to-one ;
then p' is one-to-one by A54;
then reconsider p' = p' as Permutation of (dom (Del f1,i)) by A53;
set p'' = (((Sgm ((dom f2) \ {j})) " ) * (p " )) * (Sgm ((dom f1) \ {i}));
A55: Sgm ((dom f2) \ {j}) is one-to-one by A25, FINSEQ_3:99;
set R1 = (Sgm ((dom f2) \ {j})) " ;
set R2 = Sgm ((dom f2) \ {j});
set R3 = (Sgm ((dom f1) \ {i})) " ;
set R4 = Sgm ((dom f1) \ {i});
set R5 = p " ;
set R6 = p;
set R7 = p';
reconsider R1 = (Sgm ((dom f2) \ {j})) " , R2 = Sgm ((dom f2) \ {j}), R3 = (Sgm ((dom f1) \ {i})) " , R4 = Sgm ((dom f1) \ {i}), R5 = p " , R6 = p, R7 = p', p' = p', p'' = (((Sgm ((dom f2) \ {j})) " ) * (p " )) * (Sgm ((dom f1) \ {i})) as Function ;
A56: R3 = R4 ~ by A35, FUNCT_1:def 9;
A57: R5 = R6 ~ by FUNCT_1:def 9;
reconsider R1 = R1, R2 = R2, R3 = R3, R4 = R4, R5 = R5, R6 = R6, R7 = R7 as Relation ;
p' " = R7 ~ by FUNCT_1:def 9
.= ((R6 * R3) ~ ) * (R2 ~ ) by RELAT_1:54
.= ((R3 ~ ) * (R6 ~ )) * (R2 ~ ) by RELAT_1:54
.= (((R4 ~ ) ~ ) * R5) * R1 by A55, A56, A57, FUNCT_1:def 9
.= p'' by RELAT_1:55 ;
hence ( (((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j})) is Permutation of (dom (Del f1,i)) & ((((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j}))) " = (((Sgm ((dom f2) \ {j})) " ) * (p " )) * (Sgm ((dom f1) \ {i})) ) ; :: thesis: verum

end;

then reconsider p' = (((Sgm ((dom f1) \ {i})) " ) * p) * (Sgm ((dom f2) \ {j})) as Permutation of (dom (Del f1,i)) ;
take p' ; :: thesis: Del f1,i, Del f2,j are_equivalent_under p',O

now

let H1, H2 be GroupWithOperators of O; :: thesis: for l, n being Nat st l in dom (Del f1,i) & n = (p' " ) . l & H1 = (Del f1,i) . l & H2 = (Del f2,j) . n holds
H1,H2 are_isomorphic
let l, n be Nat; :: thesis: ( l in dom (Del f1,i) & n = (p' " ) . l & H1 = (Del f1,i) . l & H2 = (Del f2,j) . n implies H1,H2 are_isomorphic )
assume A58: l in dom (Del f1,i) ; :: thesis: ( n = (p' " ) . l & H1 = (Del f1,i) . l & H2 = (Del f2,j) . n implies H1,H2 are_isomorphic )
assume A59: n = (p' " ) . l ; :: thesis: ( H1 = (Del f1,i) . l & H2 = (Del f2,j) . n implies H1,H2 are_isomorphic )
assume A60: ( H1 = (Del f1,i) . l & H2 = (Del f2,j) . n ) ; :: thesis: H1,H2 are_isomorphic
A61: l in dom (p' " ) by A58, FUNCT_2:def 1;
then n in rng (p' " ) by A59, FUNCT_1:12;
then n in dom (Del f1,i) ;
then n in Seg (len (Del f2,j)) by A8, A13, A14, FINSEQ_1:def 3;
then A62: n in dom (Del f2,j) by FINSEQ_1:def 3;
A63: dom (Del f1,i) c= dom (Sgm ((dom f1) \ {i})) by RELAT_1:44;
A64: dom (Del f2,j) c= dom (Sgm ((dom f2) \ {j})) by RELAT_1:44;
set l1 = (Sgm ((dom f1) \ {i})) . l;
set n1 = (Sgm ((dom f2) \ {j})) . n;
(Sgm ((dom f1) \ {i})) . l in rng (Sgm ((dom f1) \ {i})) by A58, A63, FUNCT_1:12;
then A65: (Sgm ((dom f1) \ {i})) . l in dom f1 by A22, XBOOLE_0:def 5;
reconsider l1 = (Sgm ((dom f1) \ {i})) . l as Nat ;
reconsider n1 = (Sgm ((dom f2) \ {j})) . n as Nat ;
A66: H1 = f1 . l1 by A58, A60, A63, FUNCT_1:23;
A67: H2 = f2 . n1 by A60, A62, A64, FUNCT_1:23;
A68: (Sgm ((dom f2) \ {j})) * (p' " ) = (Sgm ((dom f2) \ {j})) * (((Sgm ((dom f2) \ {j})) " ) * ((p " ) * (Sgm ((dom f1) \ {i})))) by A34, RELAT_1:55
.= ((Sgm ((dom f2) \ {j})) * ((Sgm ((dom f2) \ {j})) " )) * ((p " ) * (Sgm ((dom f1) \ {i}))) by RELAT_1:55
.= (id ((dom f2) \ {j})) * ((p " ) * (Sgm ((dom f1) \ {i}))) by A27, A28, A29, A33, FUNCT_2:35
.= ((id ((dom f2) \ {j})) * (p " )) * (Sgm ((dom f1) \ {i})) by RELAT_1:55
.= (((dom f2) \ {j}) | (p " )) * (Sgm ((dom f1) \ {i})) by RELAT_1:123 ;
A69: dom f1 = rng p by FUNCT_2:def 3;
then A70: l1 in dom (p " ) by A65, FUNCT_1:55;
then A71: (p " ) . l1 in rng (p " ) by FUNCT_1:12;

now

assume (p " ) . l1 in {j} ; :: thesis: contradiction
then A72: (p " ) . l1 = (p " ) . i by A5, TARSKI:def 1;
i in dom (p " ) by A3, A69, FUNCT_1:55;
then l1 = i by A70, A72, FUNCT_1:def 8;
then i in rng (Sgm ((dom f1) \ {i})) by A58, A63, FUNCT_1:12;
then not i in {i} by A22, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then A73: (p " ) . l1 in (dom f2) \ {j} by A23, A71, XBOOLE_0:def 5;
n1 = ((Sgm ((dom f2) \ {j})) * (p' " )) . l by A59, A61, FUNCT_1:23
.= (((dom f2) \ {j}) | (p " )) . l1 by A58, A63, A68, FUNCT_1:23
.= (p " ) . l1 by A65, A73, FUNCT_2:41 ;
hence H1,H2 are_isomorphic by A5, A65, A66, A67, Def37; :: thesis: verum

end;

hence Del f1,i, Del f2,j are_equivalent_under p',O by A8, A13, A14, Def37; :: thesis: verum

end;

end;