let O be set ; :: thesis: for f1, f2 being FinSequence
for i, j being Nat st i in dom f1 & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p ") . i ) holds
ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O

let f1, f2 be FinSequence; :: thesis: for i, j being Nat st i in dom f1 & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p ") . i ) holds
ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O

let i, j be Nat; :: thesis: ( i in dom f1 & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p ") . i ) implies ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O )

A1: ( len f1 = 0 or len f1 >= 0 + 1 ) by NAT_1:13;
assume A2: i in dom f1 ; :: thesis: ( for p being Permutation of (dom f1) holds
( not f1,f2 are_equivalent_under p,O or not j = (p ") . i ) or ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O )

given p being Permutation of (dom f1) such that A3: f1,f2 are_equivalent_under p,O and
A4: j = (p ") . i ; :: thesis: ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O
A5: len f1 = len f2 by A3;
rng (p ") c= dom f1 ;
then A6: rng (p ") c= Seg (len f1) by FINSEQ_1:def 3;
(p ") . i in rng (p ") by ;
then (p ") . i in Seg (len f1) by A6;
then A7: j in dom f2 by ;
then A8: ex k2 being Nat st
( len f2 = k2 + 1 & len (Del (f2,j)) = k2 ) by FINSEQ_3:104;
consider k1 being Nat such that
A9: len f1 = k1 + 1 and
A10: len (Del (f1,i)) = k1 by ;
per cases ( len f1 = 0 or len f1 = 1 or len f1 > 1 ) by ;
suppose A11: len f1 = 0 ; :: thesis: ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O
set p9 = the Permutation of (dom (Del (f1,i)));
take the Permutation of (dom (Del (f1,i))) ; :: thesis: Del (f1,i), Del (f2,j) are_equivalent_under the Permutation of (dom (Del (f1,i))),O
thus Del (f1,i), Del (f2,j) are_equivalent_under the Permutation of (dom (Del (f1,i))),O by ; :: thesis: verum
end;
suppose A12: len f1 = 1 ; :: thesis: ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O
reconsider p9 = {} as Function of (),() by FUNCT_2:1;
reconsider p9 = p9 as Function of {},{} ;
A13: p9 is onto ;
Del (f1,i) = {} by A9, A10, A12;
then reconsider p9 = p9 as Permutation of (dom (Del (f1,i))) by A13;
take p9 ; :: thesis: Del (f1,i), Del (f2,j) are_equivalent_under p9,O
thus Del (f1,i), Del (f2,j) are_equivalent_under p9,O by A5, A9, A10, A8; :: thesis: verum
end;
suppose A14: len f1 > 1 ; :: thesis: ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O
set Y = (dom f2) \ {j};
A15: now :: thesis: not (dom f2) \ {j} = {}
assume (dom f2) \ {j} = {} ; :: thesis: contradiction
then A16: dom f2 c= {j} by XBOOLE_1:37;
{j} c= dom f2 by ;
then A17: dom f2 = {j} by ;
consider k being Nat such that
A18: dom f2 = Seg k by FINSEQ_1:def 2;
k in NAT by ORDINAL1:def 12;
then k = len f2 by ;
then k >= 1 + 1 by ;
then Seg 2 c= Seg k by FINSEQ_1:5;
then {1,2} = {j} by ;
hence contradiction by ZFMISC_1:5; :: thesis: verum
end;
set X = (dom f1) \ {i};
set p9 = (((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}));
(dom f2) \ {j} c= dom f2 by XBOOLE_1:36;
then A19: (dom f2) \ {j} c= Seg (len f2) by FINSEQ_1:def 3;
(dom f1) \ {i} c= dom f1 by XBOOLE_1:36;
then A20: (dom f1) \ {i} c= Seg (len f1) by FINSEQ_1:def 3;
then A21: rng (Sgm ((dom f1) \ {i})) = (dom f1) \ {i} by FINSEQ_1:def 13;
(dom f2) \ {j} c= dom f2 by XBOOLE_1:36;
then (dom f2) \ {j} c= Seg (len f2) by FINSEQ_1:def 3;
then A22: ( Sgm ((dom f2) \ {j}) is one-to-one & rng (Sgm ((dom f2) \ {j})) = (dom f2) \ {j} ) by ;
A23: dom f1 = Seg (len f1) by FINSEQ_1:def 3
.= dom f2 by ;
A24: p . j = (p * (p ")) . i by
.= (id (dom f1)) . i by FUNCT_2:61
.= i by ;
A25: ( (((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
set R6 = p;
set R5 = p " ;
set R4 = Sgm ((dom f1) \ {i});
set R3 = (Sgm ((dom f1) \ {i})) " ;
set R2 = Sgm ((dom f2) \ {j});
set R1 = (Sgm ((dom f2) \ {j})) " ;
set p99 = (((Sgm ((dom f2) \ {j})) ") * (p ")) * (Sgm ((dom f1) \ {i}));
A26: {i} c= dom f1 by ;
A27: ((dom f1) \ {i}) \/ {i} = (dom f1) \/ {i} by XBOOLE_1:39
.= dom f1 by ;
card (((dom f1) \ {i}) \/ {i}) = (card ((dom f1) \ {i})) + () by ;
then A28: (card ((dom f1) \ {i})) + 1 = card (((dom f1) \ {i}) \/ {i}) by CARD_1:30
.= card (Seg (len f1)) by
.= k1 + 1 by ;
A29: {j} c= dom f2 by ;
A30: ((dom f2) \ {j}) \/ {j} = (dom f2) \/ {j} by XBOOLE_1:39
.= dom f2 by ;
A31: Sgm ((dom f1) \ {i}) is one-to-one by ;
then A32: dom ((Sgm ((dom f1) \ {i})) ") = (dom f1) \ {i} by ;
then dom ((Sgm ((dom f1) \ {i})) ") c= dom f1 by XBOOLE_1:36;
then A33: dom ((Sgm ((dom f1) \ {i})) ") c= rng p by FUNCT_2:def 3;
A34: now :: thesis: for x being object st x in (dom f2) \ {j} holds
x in dom (((Sgm ((dom f1) \ {i})) ") * p)
let x be object ; :: thesis: ( x in (dom f2) \ {j} implies x in dom (((Sgm ((dom f1) \ {i})) ") * p) )
assume A35: x in (dom f2) \ {j} ; :: thesis: x in dom (((Sgm ((dom f1) \ {i})) ") * p)
dom f1 = dom p by ;
then A36: x in dom p by ;
not x in {j} by ;
then x <> j by TARSKI:def 1;
then p . x <> i by ;
then A37: not p . x in {i} by TARSKI:def 1;
dom f1 = rng p by FUNCT_2:def 3;
then p . x in dom f1 by ;
then p . x in (dom f1) \ {i} by ;
hence x in dom (((Sgm ((dom f1) \ {i})) ") * p) by ; :: thesis: verum
end;
now :: thesis: for x being object st x in dom (((Sgm ((dom f1) \ {i})) ") * p) holds
x in (dom f2) \ {j}
let x be object ; :: thesis: ( x in dom (((Sgm ((dom f1) \ {i})) ") * p) implies x in (dom f2) \ {j} )
assume A38: x in dom (((Sgm ((dom f1) \ {i})) ") * p) ; :: thesis: x in (dom f2) \ {j}
then p . x in dom ((Sgm ((dom f1) \ {i})) ") by FUNCT_1:11;
then p . x in (dom f1) \ {i} by ;
then not p . x in {i} by XBOOLE_0:def 5;
then p . x <> i by TARSKI:def 1;
then A39: not x in {j} by ;
x in dom p by ;
hence x in (dom f2) \ {j} by ; :: thesis: verum
end;
then dom (((Sgm ((dom f1) \ {i})) ") * p) = (dom f2) \ {j} by ;
then A40: dom (((Sgm ((dom f1) \ {i})) ") * p) = rng (Sgm ((dom f2) \ {j})) by ;
then rng ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = rng (((Sgm ((dom f1) \ {i})) ") * p) by RELAT_1:28
.= rng ((Sgm ((dom f1) \ {i})) ") by
.= dom (Sgm ((dom f1) \ {i})) by ;
then A41: rng ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by ;
card (((dom f2) \ {j}) \/ {j}) = (card ((dom f2) \ {j})) + () by ;
then (card ((dom f2) \ {j})) + 1 = card (((dom f2) \ {j}) \/ {j}) by CARD_1:30
.= card (Seg (len f2)) by
.= k1 + 1 by ;
then dom (Sgm ((dom f2) \ {j})) = Seg k1 by ;
then A42: dom ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by ;
A43: dom (Del (f1,i)) = Seg k1 by ;
then reconsider p9 = (((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j})) as Function of (dom (Del (f1,i))),(dom (Del (f1,i))) by ;
A44: p9 is onto by ;
Sgm ((dom f2) \ {j}) is one-to-one by ;
then reconsider p9 = p9 as Permutation of (dom (Del (f1,i))) by ;
set R7 = p9;
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 = p9, p9 = p9, p99 = (((Sgm ((dom f2) \ {j})) ") * (p ")) * (Sgm ((dom f1) \ {i})) as Function ;
A45: R3 = R4 ~ by ;
A46: ( Sgm ((dom f2) \ {j}) is one-to-one & R5 = R6 ~ ) by ;
reconsider R1 = R1, R2 = R2, R3 = R3, R4 = R4, R5 = R5, R6 = R6, R7 = R7 as Relation ;
p9 " = R7 ~ by FUNCT_1:def 5
.= ((R6 * R3) ~) * (R2 ~) by RELAT_1:35
.= ((R3 ~) * (R6 ~)) * (R2 ~) by RELAT_1:35
.= (((R4 ~) ~) * R5) * R1 by
.= p99 by RELAT_1:36 ;
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 p9 = (((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j})) as Permutation of (dom (Del (f1,i))) ;
take p9 ; :: thesis: Del (f1,i), Del (f2,j) are_equivalent_under p9,O
A47: Sgm ((dom f2) \ {j}) is Function of (dom (Sgm ((dom f2) \ {j}))),(rng (Sgm ((dom f2) \ {j}))) by FUNCT_2:1;
now :: thesis: for H1, H2 being GroupWithOperators of O
for l, n being Nat st l in dom (Del (f1,i)) & n = (p9 ") . l & H1 = (Del (f1,i)) . l & H2 = (Del (f2,j)) . n holds
H1,H2 are_isomorphic
let H1, H2 be GroupWithOperators of O; :: thesis: for l, n being Nat st l in dom (Del (f1,i)) & n = (p9 ") . 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 = (p9 ") . l & H1 = (Del (f1,i)) . l & H2 = (Del (f2,j)) . n implies H1,H2 are_isomorphic )
assume A48: l in dom (Del (f1,i)) ; :: thesis: ( n = (p9 ") . l & H1 = (Del (f1,i)) . l & H2 = (Del (f2,j)) . n implies H1,H2 are_isomorphic )
set n1 = (Sgm ((dom f2) \ {j})) . n;
reconsider n1 = (Sgm ((dom f2) \ {j})) . n as Nat ;
A49: (Sgm ((dom f2) \ {j})) * (p9 ") = (Sgm ((dom f2) \ {j})) * (((Sgm ((dom f2) \ {j})) ") * ((p ") * (Sgm ((dom f1) \ {i})))) by
.= ((Sgm ((dom f2) \ {j})) * ((Sgm ((dom f2) \ {j})) ")) * ((p ") * (Sgm ((dom f1) \ {i}))) by RELAT_1:36
.= (id ((dom f2) \ {j})) * ((p ") * (Sgm ((dom f1) \ {i}))) by
.= ((id ((dom f2) \ {j})) * (p ")) * (Sgm ((dom f1) \ {i})) by RELAT_1:36
.= (((dom f2) \ {j}) |` (p ")) * (Sgm ((dom f1) \ {i})) by RELAT_1:92 ;
assume A50: n = (p9 ") . l ; :: thesis: ( H1 = (Del (f1,i)) . l & H2 = (Del (f2,j)) . n implies H1,H2 are_isomorphic )
A51: l in dom (p9 ") by ;
then n in rng (p9 ") by ;
then n in dom (Del (f1,i)) ;
then n in Seg (len (Del (f2,j))) by ;
then A52: n in dom (Del (f2,j)) by FINSEQ_1:def 3;
set l1 = (Sgm ((dom f1) \ {i})) . l;
A53: dom (Del (f1,i)) c= dom (Sgm ((dom f1) \ {i})) by RELAT_1:25;
then (Sgm ((dom f1) \ {i})) . l in rng (Sgm ((dom f1) \ {i})) by ;
then A54: (Sgm ((dom f1) \ {i})) . l in dom f1 by ;
assume that
A55: H1 = (Del (f1,i)) . l and
A56: H2 = (Del (f2,j)) . n ; :: thesis: H1,H2 are_isomorphic
reconsider l1 = (Sgm ((dom f1) \ {i})) . l as Nat ;
A57: H1 = f1 . l1 by ;
A58: dom f1 = rng p by FUNCT_2:def 3;
then A59: l1 in dom (p ") by ;
A60: now :: thesis: not (p ") . l1 in {j}
assume (p ") . l1 in {j} ; :: thesis: contradiction
then A61: (p ") . l1 = (p ") . i by ;
i in dom (p ") by ;
then l1 = i by ;
then i in rng (Sgm ((dom f1) \ {i})) by ;
then not i in {i} by ;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
(p ") . l1 in rng (p ") by ;
then A62: (p ") . l1 in (dom f2) \ {j} by ;
dom (Del (f2,j)) c= dom (Sgm ((dom f2) \ {j})) by RELAT_1:25;
then A63: H2 = f2 . n1 by ;
n1 = ((Sgm ((dom f2) \ {j})) * (p9 ")) . l by
.= (((dom f2) \ {j}) |` (p ")) . l1 by
.= (p ") . l1 by ;
hence H1,H2 are_isomorphic by A3, A54, A57, A63; :: thesis: verum
end;
hence Del (f1,i), Del (f2,j) are_equivalent_under p9,O by A5, A9, A10, A8; :: thesis: verum
end;
end;