let F be non empty FinSequence; :: thesis:
let G be FinSequence; :: thesis:
assume A1: rng G c= rng F ; :: thesis:
defpred S₁[ Nat] means ( $1 <= len G implies ex o being len F -element DoubleReorganization of Seg $1 st
for k being Nat holds
( o . k is increasing & F . k = G . (o _ (k,1)) & ... & F . k = G . (o _ (k,(len (o . k)))) ) );
A2: S₁[ 0 ]

proof

assume 0 <= len G ; :: thesis:
take o = the len F -element DoubleReorganization of Seg 0; :: thesis:
let i be Nat; :: thesis:
thus o . i is increasing ; :: thesis:
let j be Nat; :: thesis:
thus ( not 1 <= j or not j <= len (o . i) or F . i = G . (o _ (i,j)) ) ; :: thesis:

end;

A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
set i1 = i + 1;
assume A4: S₁[i] ; :: thesis:
assume A5: i + 1 <= len G ; :: thesis:
then consider o being len F -element DoubleReorganization of Seg i such that
A6: for j being Nat holds
( o . j is increasing & F . j = G . (o _ (j,1)) & ... & F . j = G . (o _ (j,(len (o . j)))) ) by NAT_1:13, A4;
A7: len o = len F by CARD_1:def 7;
then A8: dom o = dom F by FINSEQ_3:29;
A9: Values o = Seg i by Def7;
i + 1 in dom G by NAT_1:11, A5, FINSEQ_3:25;
then G . (i + 1) in rng G by FUNCT_1:def 3;
then consider x being object such that
A10: ( x in dom F & F . x = G . (i + 1) ) by A1, FUNCT_1:def 3;
reconsider x = x as Nat by A10;
set ox = o . x;
set I1 = <*(i + 1)*>;
set oxI = (o . x) ^ <*(i + 1)*>;
A11: i < i + 1 by NAT_1:13;
not i + 1 in rng (o . x)

proof

assume i + 1 in rng (o . x) ; :: thesis:
then consider y being object such that
A12: ( y in dom (o . x) & i + 1 = (o . x) . y ) by FUNCT_1:def 3;
i + 1 in Seg i by Th1, A10, A8, A9, A12;
hence contradiction by FINSEQ_1:1, A11; :: thesis:

end;

then A13: (o . x) ^ <*(i + 1)*> is one-to-one by GRAPHSP:1;
A14: x in dom o by A10, A7, FINSEQ_3:29;
o . x in rng o by A10, A8, FUNCT_1:def 3;
then A15: o . x is FinSequence of Seg i by FINSEQ_1:def 11;
then A16: rng (o . x) c= Seg i by FINSEQ_1:def 4;
A17: (rng (o . x)) /\ (Seg i) = rng (o . x) by A15, FINSEQ_1:def 4, XBOOLE_1:28;
not i + 1 in Seg i by A11, FINSEQ_1:1;
then A18: {(i + 1)} misses Seg i by ZFMISC_1:52, ZFMISC_1:45;
A19: rng <*(i + 1)*> = {(i + 1)} by FINSEQ_1:39;
then rng ((o . x) ^ <*(i + 1)*>) = (rng (o . x)) \/ {(i + 1)} by FINSEQ_1:31;
then A20: (rng ((o . x) ^ <*(i + 1)*>)) /\ (Seg i) = (rng (o . x)) \/ {} by A17, A18, XBOOLE_1:23;
A21: (Seg i) \/ {(i + 1)} = Seg (i + 1) by FINSEQ_1:9;
Seg i c= {(i + 1)} \/ (Seg i) by XBOOLE_1:7;
then A22: rng (o . x) c= {(i + 1)} \/ (Seg i) by A16;
set O = o +* (x,((o . x) ^ <*(i + 1)*>));
(rng ((o . x) ^ <*(i + 1)*>)) \/ ((Seg i) \ (rng (o . x))) = ((rng (o . x)) \/ {(i + 1)}) \/ ((Seg i) \ (rng (o . x))) by A19, FINSEQ_1:31
.= (rng (o . x)) \/ ({(i + 1)} \/ ((Seg i) \ (rng (o . x)))) by XBOOLE_1:4
.= (rng (o . x)) \/ (({(i + 1)} \/ (Seg i)) \ (rng (o . x))) by A16, A18, XBOOLE_1:63, XBOOLE_1:87
.= (rng (o . x)) \/ ({(i + 1)} \/ (Seg i)) by XBOOLE_1:39
.= {(i + 1)} \/ (Seg i) by A22, XBOOLE_1:12 ;
then reconsider O = o +* (x,((o . x) ^ <*(i + 1)*>)) as len F -element DoubleReorganization of Seg (i + 1) by A13, A14, Th37, A20, A21;
take O ; :: thesis:
let k be Nat; :: thesis:
set Ok = O . k;
A23: ( dom <*(i + 1)*> = Seg 1 & Seg 1 = {1} & <*(i + 1)*> . 1 = i + 1 ) by FINSEQ_1:38, FINSEQ_1:2;
thus O . k is increasing :: thesis:

proof

per cases ;

suppose k <> x ; :: thesis:

then O . k = o . k by FUNCT_7:32;
hence O . k is increasing by A6; :: thesis:

end;

suppose k = x ; :: thesis:

then A24: O . k = (o . x) ^ <*(i + 1)*> by A10, A8, FUNCT_7:31;
let e1, e2 be ExtReal; :: according to VALUED_0:def 13 :: thesis:
assume A25: ( e1 in dom (O . k) & e2 in dom (O . k) & e1 < e2 ) ; :: thesis:

per cases ;

suppose A26: ( e1 in dom (o . x) & e2 in dom (o . x) ) ; :: thesis:

then ( (O . k) . e1 = (o . x) . e1 & (O . k) . e2 = (o . x) . e2 & o . x is increasing ) by A6, A24, FINSEQ_1:def 7;
hence (O . k) . e1 < (O . k) . e2 by A25, A26, VALUED_0:def 13; :: thesis:

end;

suppose ( not e1 in dom (o . x) & e2 in dom (o . x) ) ; :: thesis:

then ( e2 <= len (o . x) & 1 <= e1 & ( 1 > e1 or e1 > len (o . x) ) ) by A25, FINSEQ_3:25;
hence not (O . k) . e2 <= (O . k) . e1 by XXREAL_0:2, A25; :: thesis:

end;

suppose A27: ( e1 in dom (o . x) & not e2 in dom (o . x) ) ; :: thesis:

then consider n being Nat such that
A28: ( n in dom <*(i + 1)*> & e2 = (len (o . x)) + n ) by A24, A25, FINSEQ_1:25;
n = 1 by A23, A28, TARSKI:def 1;
then A29: ((o . x) ^ <*(i + 1)*>) . e2 = i + 1 by A28, FINSEQ_1:def 7, A23;
A30: (o . x) . e1 = ((o . x) ^ <*(i + 1)*>) . e1 by A27, FINSEQ_1:def 7;
(o . x) . e1 in Seg i by A10, A8, Th1, A9, A27;
then (o . x) . e1 <= i by FINSEQ_1:1;
hence not (O . k) . e2 <= (O . k) . e1 by A29, A30, NAT_1:13, A24; :: thesis:

end;

suppose A31: ( not e1 in dom (o . x) & not e2 in dom (o . x) ) ; :: thesis:

then consider n being Nat such that
A32: ( n in dom <*(i + 1)*> & e1 = (len (o . x)) + n ) by A24, A25, FINSEQ_1:25;
consider k being Nat such that
A33: ( k in dom <*(i + 1)*> & e2 = (len (o . x)) + k ) by A24, A31, A25, FINSEQ_1:25;
( n = 1 & k = 1 ) by A33, A23, A32, TARSKI:def 1;
hence not (O . k) . e2 <= (O . k) . e1 by A32, A33, A25; :: thesis:

end;

thus F . k = G . (O _ (k,1)) & ... & F . k = G . (O _ (k,(len (O . k)))) :: thesis:

proof

let j be Nat; :: thesis:
assume A34: ( 1 <= j & j <= len (O . k) ) ; :: thesis:
A35: F . k = G . (o _ (k,1)) & ... & F . k = G . (o _ (k,(len (o . k)))) by A6;

per cases ;

suppose A36: k <> x ; :: thesis:

then O . k = o . k by FUNCT_7:32;
then F . k = G . (o _ (k,j)) by A34, A35;
hence F . k = G . (O _ (k,j)) by A36, FUNCT_7:32; :: thesis:

end;

suppose A37: k = x ; :: thesis:

then A38: O . k = (o . x) ^ <*(i + 1)*> by A10, A8, FUNCT_7:31;

per cases ;

suppose A39: j in dom (o . x) ; :: thesis:

then A40: ( ((o . x) ^ <*(i + 1)*>) . j = (o . x) . j & j <= len (o . x) ) by FINSEQ_1:def 7, FINSEQ_3:25;
o _ (k,j) = ((o . x) ^ <*(i + 1)*>) . j by A37, A39, FINSEQ_1:def 7
.= (O . k) . j by A37, A14, FUNCT_7:31 ;
hence F . k = G . (O _ (k,j)) by A40, A37, A35, A34; :: thesis:

end;

suppose not j in dom (o . x) ; :: thesis:

then consider n being Nat such that
A41: ( n in dom <*(i + 1)*> & j = (len (o . x)) + n ) by A38, A34, FINSEQ_3:25, FINSEQ_1:25;
n = 1 by A23, A41, TARSKI:def 1;
then F . k = G . (((o . x) ^ <*(i + 1)*>) . j) by A41, A23, FINSEQ_1:def 7, A10, A37
.= G . ((O . k) . j) by A37, A14, FUNCT_7:31 ;
hence F . k = G . (O _ (k,j)) ; :: thesis:

end;

A42: dom G = Seg (len G) by FINSEQ_1:def 3;
for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
then ex o being len F -element DoubleReorganization of dom G st
for k being Nat holds
( o . k is increasing & F . k = G . (o _ (k,1)) & ... & F . k = G . (o _ (k,(len (o . k)))) ) by A42;
hence ex o being len F -element DoubleReorganization of dom G st
for n being Nat holds
( o . n is increasing & F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n)))) ) ; :: thesis: