let O be set ; :: thesis:
let f1, f2 be FinSequence; :: thesis:
let i, j be Nat; :: thesis:
A3: ( len f1 = 0 or len f1 >= 0 + 1 ) by NAT_1:13;
assume A4: i in dom f1 ; :: thesis:
given p being Permutation of (dom f1) such that A6: f1,f2 are_equivalent_under p,O and
A7: j = (p ") . i ; :: thesis:
A8: len f1 = len f2 by A6, Def37;
rng (p ") c= dom f1 ;
then A9: rng (p ") c= Seg (len f1) by FINSEQ_1:def 3;
(p ") . i in rng (p ") by A4, FUNCT_2:4;
then (p ") . i in Seg (len f1) by A9;
then A10: j in dom f2 by A7, A8, FINSEQ_1:def 3;
then A11: ex k2 being Nat st
( len f2 = k2 + 1 & len (Del (f2,j)) = k2 ) by FINSEQ_3:104;
consider k1 being Nat such that
A12: len f1 = k1 + 1 and
A13: len (Del (f1,i)) = k1 by A4, FINSEQ_3:104;

per cases by A3, XXREAL_0:1;

suppose A14: len f1 = 0 ; :: thesis:

set p9 = the Permutation of (dom (Del (f1,i)));
take the Permutation of (dom (Del (f1,i))) ; :: thesis:
thus Del (f1,i), Del (f2,j) are_equivalent_under the Permutation of (dom (Del (f1,i))),O by A12, A14; :: thesis:

end;

suppose A15: len f1 = 1 ; :: thesis:

reconsider p9 = {} as Function of (dom {}),(rng {}) by FUNCT_2:1;
reconsider p9 = p9 as Function of {},{} ;
A16: p9 is onto by FUNCT_2:def 3;
Del (f1,i) = {} by A12, A13, A15;
then reconsider p9 = p9 as Permutation of (dom (Del (f1,i))) by A16;
take p9 ; :: 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 ;
hence Del (f1,i), Del (f2,j) are_equivalent_under p9,O by A8, A12, A13, A11, Def37; :: thesis:

end;

suppose A17: len f1 > 1 ; :: thesis:

set Y = (dom f2) \ {j};

A18: now

assume (dom f2) \ {j} = {} ; :: thesis:
then A19: dom f2 c= {j} by XBOOLE_1:37;
{j} c= dom f2 by A10, ZFMISC_1:31;
then A20: dom f2 = {j} by A19, XBOOLE_0:def 10;
consider k being Nat such that
A21: dom f2 = Seg k by FINSEQ_1:def 2;
k in NAT by ORDINAL1:def 12;
then k = len f2 by A21, FINSEQ_1:def 3;
then k >= 1 + 1 by A8, A17, NAT_1:13;
then Seg 2 c= Seg k by FINSEQ_1:5;
then {1,2} = {j} by A20, A21, FINSEQ_1:2, ZFMISC_1:21;
hence contradiction by ZFMISC_1:5; :: thesis:

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 A22: (dom f2) \ {j} c= Seg (len f2) by FINSEQ_1:def 3;
(dom f1) \ {i} c= dom f1 by XBOOLE_1:36;
then A23: (dom f1) \ {i} c= Seg (len f1) by FINSEQ_1:def 3;
then A24: 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 A25: ( Sgm ((dom f2) \ {j}) is one-to-one & rng (Sgm ((dom f2) \ {j})) = (dom f2) \ {j} ) by FINSEQ_1:def 13, FINSEQ_3:92;
A26: dom f1 = Seg (len f1) by FINSEQ_1:def 3
.= Seg (len f2) by A6, Def37
.= dom f2 by FINSEQ_1:def 3 ;
A27: p . j = (p * (p ")) . i by A4, A7, FUNCT_2:15
.= (id (dom f1)) . i by FUNCT_2:61
.= i by A4, FUNCT_1:18 ;
A28: ( (((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}));
A29: {i} c= dom f1 by A4, ZFMISC_1:31;
A30: ((dom f1) \ {i}) \/ {i} = (dom f1) \/ {i} by XBOOLE_1:39
.= dom f1 by A29, XBOOLE_1:12 ;
card (((dom f1) \ {i}) \/ {i}) = (card ((dom f1) \ {i})) + (card {i}) by CARD_2:40, XBOOLE_1:79;
then A31: (card ((dom f1) \ {i})) + 1 = card (((dom f1) \ {i}) \/ {i}) by CARD_1:30
.= card (Seg (len f1)) by A30, FINSEQ_1:def 3
.= k1 + 1 by A12, FINSEQ_1:57 ;
A32: {j} c= dom f2 by A10, ZFMISC_1:31;
A33: ((dom f2) \ {j}) \/ {j} = (dom f2) \/ {j} by XBOOLE_1:39
.= dom f2 by A32, XBOOLE_1:12 ;
A34: Sgm ((dom f1) \ {i}) is one-to-one by A23, FINSEQ_3:92;
then A35: dom ((Sgm ((dom f1) \ {i})) ") = (dom f1) \ {i} by A24, FUNCT_1:33;
then dom ((Sgm ((dom f1) \ {i})) ") c= dom f1 by XBOOLE_1:36;
then A36: dom ((Sgm ((dom f1) \ {i})) ") c= rng p by FUNCT_2:def 3;

A37: now

let x be set ; :: thesis:
assume A38: x in (dom f2) \ {j} ; :: thesis:
dom f1 = dom p by A4, FUNCT_2:def 1;
then A39: x in dom p by A26, A38, XBOOLE_0:def 5;
not x in {j} by A38, XBOOLE_0:def 5;
then x <> j by TARSKI:def 1;
then p . x <> i by A10, A26, A27, A39, FUNCT_2:56;
then A40: 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 A39, FUNCT_1:3;
then p . x in (dom f1) \ {i} by A40, XBOOLE_0:def 5;
hence x in dom (((Sgm ((dom f1) \ {i})) ") * p) by A35, A39, FUNCT_1:11; :: thesis:

end;

now

let x be set ; :: thesis:
assume A41: x in dom (((Sgm ((dom f1) \ {i})) ") * p) ; :: thesis:
then p . x in dom ((Sgm ((dom f1) \ {i})) ") by FUNCT_1:11;
then p . x in (dom f1) \ {i} by A24, A34, FUNCT_1:33;
then not p . x in {i} by XBOOLE_0:def 5;
then p . x <> i by TARSKI:def 1;
then A42: not x in {j} by A27, TARSKI:def 1;
x in dom p by A41, FUNCT_1:11;
hence x in (dom f2) \ {j} by A26, A42, XBOOLE_0:def 5; :: thesis:

end;

then dom (((Sgm ((dom f1) \ {i})) ") * p) = (dom f2) \ {j} by A37, TARSKI:1;
then A43: dom (((Sgm ((dom f1) \ {i})) ") * p) = rng (Sgm ((dom f2) \ {j})) by A22, FINSEQ_1:def 13;
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 A36, RELAT_1:28
.= dom (Sgm ((dom f1) \ {i})) by A34, FUNCT_1:33 ;
then A44: rng ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by A23, A31, FINSEQ_3:40;
card (((dom f2) \ {j}) \/ {j}) = (card ((dom f2) \ {j})) + (card {j}) by CARD_2:40, XBOOLE_1:79;
then (card ((dom f2) \ {j})) + 1 = card (((dom f2) \ {j}) \/ {j}) by CARD_1:30
.= card (Seg (len f2)) by A33, FINSEQ_1:def 3
.= card (Seg (len f1)) by A6, Def37
.= k1 + 1 by A12, FINSEQ_1:57 ;
then dom (Sgm ((dom f2) \ {j})) = Seg k1 by A22, FINSEQ_3:40;
then A45: dom ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by A43, RELAT_1:27;
A46: dom (Del (f1,i)) = Seg k1 by A13, FINSEQ_1:def 3;
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, A45, FUNCT_2:1;
A47: p9 is onto by A46, A44, FUNCT_2:def 3;
Sgm ((dom f2) \ {j}) is one-to-one by A22, FINSEQ_3:92;
then reconsider p9 = p9 as Permutation of (dom (Del (f1,i))) by A34, A47;
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 ;
A48: R3 = R4 ~ by A34, FUNCT_1:def 5;
A49: ( Sgm ((dom f2) \ {j}) is one-to-one & R5 = R6 ~ ) by A22, FINSEQ_3:92, FUNCT_1:def 5;
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 A48, A49, FUNCT_1:def 5
.= 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:

end;

then reconsider p9 = (((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j})) as Permutation of (dom (Del (f1,i))) ;
take p9 ; :: thesis:
A50: Sgm ((dom f2) \ {j}) is Function of (dom (Sgm ((dom f2) \ {j}))),(rng (Sgm ((dom f2) \ {j}))) by FUNCT_2:1;

now

let H1, H2 be GroupWithOperators of O; :: thesis:
let l, n be Nat; :: thesis:
assume A51: l in dom (Del (f1,i)) ; :: thesis:
set n1 = (Sgm ((dom f2) \ {j})) . n;
reconsider n1 = (Sgm ((dom f2) \ {j})) . n as Nat ;
A52: (Sgm ((dom f2) \ {j})) * (p9 ") = (Sgm ((dom f2) \ {j})) * (((Sgm ((dom f2) \ {j})) ") * ((p ") * (Sgm ((dom f1) \ {i})))) by A28, RELAT_1:36
.= ((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 A25, A18, A50, FUNCT_2:29
.= ((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 A53: n = (p9 ") . l ; :: thesis:
A54: l in dom (p9 ") by A51, FUNCT_2:def 1;
then n in rng (p9 ") by A53, FUNCT_1:3;
then n in dom (Del (f1,i)) ;
then n in Seg (len (Del (f2,j))) by A8, A12, A13, A11, FINSEQ_1:def 3;
then A55: n in dom (Del (f2,j)) by FINSEQ_1:def 3;
set l1 = (Sgm ((dom f1) \ {i})) . l;
A56: 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 A51, FUNCT_1:3;
then A57: (Sgm ((dom f1) \ {i})) . l in dom f1 by A24, XBOOLE_0:def 5;
assume that
A58: H1 = (Del (f1,i)) . l and
A59: H2 = (Del (f2,j)) . n ; :: thesis:
reconsider l1 = (Sgm ((dom f1) \ {i})) . l as Nat ;
A60: H1 = f1 . l1 by A51, A58, A56, FUNCT_1:13;
A61: dom f1 = rng p by FUNCT_2:def 3;
then A62: l1 in dom (p ") by A57, FUNCT_1:33;

A63: now

assume (p ") . l1 in {j} ; :: thesis:
then A64: (p ") . l1 = (p ") . i by A7, TARSKI:def 1;
i in dom (p ") by A4, A61, FUNCT_1:33;
then l1 = i by A62, A64, FUNCT_1:def 4;
then i in rng (Sgm ((dom f1) \ {i})) by A51, A56, FUNCT_1:3;
then not i in {i} by A24, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

(p ") . l1 in rng (p ") by A62, FUNCT_1:3;
then A65: (p ") . l1 in (dom f2) \ {j} by A26, A63, XBOOLE_0:def 5;
dom (Del (f2,j)) c= dom (Sgm ((dom f2) \ {j})) by RELAT_1:25;
then A66: H2 = f2 . n1 by A59, A55, FUNCT_1:13;
n1 = ((Sgm ((dom f2) \ {j})) * (p9 ")) . l by A53, A54, FUNCT_1:13
.= (((dom f2) \ {j}) | (p ")) . l1 by A51, A56, A52, FUNCT_1:13
.= (p ") . l1 by A57, A65, FUNCT_2:34 ;
hence H1,H2 are_isomorphic by A6, A57, A60, A66, Def37; :: thesis:

end;

hence Del (f1,i), Del (f2,j) are_equivalent_under p9,O by A8, A12, A13, A11, Def37; :: thesis:

end;