let O be set ; :: thesis:
let f1, f2 be FinSequence; :: thesis:
let i, j be Nat; :: thesis:
A1: ( len f1 = 0 or len f1 >= 0 + 1 ) by NAT_1:13;
assume A2: i in dom f1 ; :: thesis:
given p being Permutation of (dom f1) such that A3: f1,f2 are_equivalent_under p,O and
A4: j = (p ") . i ; :: thesis:
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 A2, FUNCT_2:4;
then (p ") . i in Seg (len f1) by A6;
then A7: j in dom f2 by A4, A5, FINSEQ_1:def 3;
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 A2, FINSEQ_3:104;

per cases by A1, XXREAL_0:1;

suppose A11: 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 A9, A11; :: thesis:

end;

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

reconsider p9 = {} as Function of (dom {}),(rng {}) 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:
thus Del (f1,i), Del (f2,j) are_equivalent_under p9,O by A5, A9, A10, A8; :: thesis:

end;

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

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

A15: now :: thesis:

assume (dom f2) \ {j} = {} ; :: thesis:
then A16: dom f2 c= {j} by XBOOLE_1:37;
{j} c= dom f2 by A7, ZFMISC_1:31;
then A17: dom f2 = {j} by A16, XBOOLE_0:def 10;
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 A18, FINSEQ_1:def 3;
then k >= 1 + 1 by A5, A14, NAT_1:13;
then Seg 2 c= Seg k by FINSEQ_1:5;
then {1,2} = {j} by A17, A18, 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 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 FINSEQ_1:def 13, FINSEQ_3:92;
A23: dom f1 = Seg (len f1) by FINSEQ_1:def 3
.= dom f2 by A3, FINSEQ_1:def 3 ;
A24: p . j = (p * (p ")) . i by A2, A4, FUNCT_2:15
.= (id (dom f1)) . i by FUNCT_2:61
.= i by A2, FUNCT_1:18 ;
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 A2, ZFMISC_1:31;
A27: ((dom f1) \ {i}) \/ {i} = (dom f1) \/ {i} by XBOOLE_1:39
.= dom f1 by A26, XBOOLE_1:12 ;
card (((dom f1) \ {i}) \/ {i}) = (card ((dom f1) \ {i})) + (card {i}) by CARD_2:40, XBOOLE_1:79;
then A28: (card ((dom f1) \ {i})) + 1 = card (((dom f1) \ {i}) \/ {i}) by CARD_1:30
.= card (Seg (len f1)) by A27, FINSEQ_1:def 3
.= k1 + 1 by A9, FINSEQ_1:57 ;
A29: {j} c= dom f2 by A7, ZFMISC_1:31;
A30: ((dom f2) \ {j}) \/ {j} = (dom f2) \/ {j} by XBOOLE_1:39
.= dom f2 by A29, XBOOLE_1:12 ;
A31: Sgm ((dom f1) \ {i}) is one-to-one by A20, FINSEQ_3:92;
then A32: dom ((Sgm ((dom f1) \ {i})) ") = (dom f1) \ {i} by A21, FUNCT_1:33;
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:

let x be object ; :: thesis:
assume A35: x in (dom f2) \ {j} ; :: thesis:
dom f1 = dom p by A2, FUNCT_2:def 1;
then A36: x in dom p by A23, A35, XBOOLE_0:def 5;
not x in {j} by A35, XBOOLE_0:def 5;
then x <> j by TARSKI:def 1;
then p . x <> i by A7, A23, A24, A36, FUNCT_2:56;
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 A36, FUNCT_1:3;
then p . x in (dom f1) \ {i} by A37, XBOOLE_0:def 5;
hence x in dom (((Sgm ((dom f1) \ {i})) ") * p) by A32, A36, FUNCT_1:11; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A38: 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 A21, A31, FUNCT_1:33;
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 A24, TARSKI:def 1;
x in dom p by A38, FUNCT_1:11;
hence x in (dom f2) \ {j} by A23, A39, XBOOLE_0:def 5; :: thesis:

end;

then dom (((Sgm ((dom f1) \ {i})) ") * p) = (dom f2) \ {j} by A34, TARSKI:2;
then A40: dom (((Sgm ((dom f1) \ {i})) ") * p) = rng (Sgm ((dom f2) \ {j})) by A19, 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 A33, RELAT_1:28
.= dom (Sgm ((dom f1) \ {i})) by A31, FUNCT_1:33 ;
then A41: rng ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by A20, A28, 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 A30, FINSEQ_1:def 3
.= k1 + 1 by A3, A9, FINSEQ_1:57 ;
then dom (Sgm ((dom f2) \ {j})) = Seg k1 by A19, FINSEQ_3:40;
then A42: dom ((((Sgm ((dom f1) \ {i})) ") * p) * (Sgm ((dom f2) \ {j}))) = Seg k1 by A40, RELAT_1:27;
A43: dom (Del (f1,i)) = Seg k1 by A10, 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 A41, A42, FUNCT_2:1;
A44: p9 is onto by A43, A41;
Sgm ((dom f2) \ {j}) is one-to-one by A19, FINSEQ_3:92;
then reconsider p9 = p9 as Permutation of (dom (Del (f1,i))) by A31, A44;
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 A31, FUNCT_1:def 5;
A46: ( Sgm ((dom f2) \ {j}) is one-to-one & R5 = R6 ~ ) by A19, 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 A45, A46, 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:
A47: Sgm ((dom f2) \ {j}) is Function of (dom (Sgm ((dom f2) \ {j}))),(rng (Sgm ((dom f2) \ {j}))) by FUNCT_2:1;

now :: thesis:

let H1, H2 be GroupWithOperators of O; :: thesis:
let l, n be Nat; :: thesis:
assume A48: l in dom (Del (f1,i)) ; :: thesis:
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 A25, 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 A22, A15, A47, 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 A50: n = (p9 ") . l ; :: thesis:
A51: l in dom (p9 ") by A48, FUNCT_2:def 1;
then n in rng (p9 ") by A50, FUNCT_1:3;
then n in dom (Del (f1,i)) ;
then n in Seg (len (Del (f2,j))) by A5, A9, A10, A8, FINSEQ_1:def 3;
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 A48, FUNCT_1:3;
then A54: (Sgm ((dom f1) \ {i})) . l in dom f1 by A21, XBOOLE_0:def 5;
assume that
A55: H1 = (Del (f1,i)) . l and
A56: H2 = (Del (f2,j)) . n ; :: thesis:
reconsider l1 = (Sgm ((dom f1) \ {i})) . l as Nat ;
A57: H1 = f1 . l1 by A48, A55, A53, FUNCT_1:13;
A58: dom f1 = rng p by FUNCT_2:def 3;
then A59: l1 in dom (p ") by A54, FUNCT_1:33;

A60: now :: thesis:

assume (p ") . l1 in {j} ; :: thesis:
then A61: (p ") . l1 = (p ") . i by A4, TARSKI:def 1;
i in dom (p ") by A2, A58, FUNCT_1:33;
then l1 = i by A59, A61, FUNCT_1:def 4;
then i in rng (Sgm ((dom f1) \ {i})) by A48, A53, FUNCT_1:3;
then not i in {i} by A21, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

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

end;

hence Del (f1,i), Del (f2,j) are_equivalent_under p9,O by A5, A9, A10, A8; :: thesis:

end;