let g be natural-valued FinSequence; :: thesis: for sort being DoubleReorganization of dom g ex h being 2 * (len b₁) -element FinSequence of NAT st
for j being Nat holds
( h . (2 * j) = 0 & h . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )
let sort be DoubleReorganization of dom g; :: thesis: ex h being 2 * (len sort) -element FinSequence of NAT st
for j being Nat holds
( h . (2 * j) = 0 & h . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )
defpred S₁[ object , object ] means for j being Nat holds
( ( $1 = (2 * j) - 1 implies $2 = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) ) & ( $1 = 2 * j implies $2 = 0 ) );
set S = Seg (2 * (len sort));
A1: for k being Nat st k in Seg (2 * (len sort)) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (2 * (len sort)) implies ex x being object st S₁[k,x] )
assume k in Seg (2 * (len sort)) ; :: thesis: ex x being object st S₁[k,x]

per cases ( k is even or k is odd ) ;

suppose A2: k is even ; :: thesis: ex x being object st S₁[k,x]

set j = the Nat;
take x = 0 ; :: thesis: S₁[k,x]
thus S₁[k,x] by A2; :: thesis: verum

end;

suppose k is odd ; :: thesis: ex x being object st S₁[k,x]

then consider j being Nat such that
A4: k = (2 * j) + 1 by ABIAN:9;
set j1 = j + 1;
take x = (g . (sort _ ((j + 1),1))) + ((((g *. sort) . (j + 1)),2) +...); :: thesis: S₁[k,x]
let i be Nat; :: thesis: ( ( k = (2 * i) - 1 implies x = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) ) & ( k = 2 * i implies x = 0 ) )
thus ( ( k = (2 * i) - 1 implies x = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) ) & ( k = 2 * i implies x = 0 ) ) by A4; :: thesis: verum

end;

end;

end;

consider f being FinSequence such that
A5: ( dom f = Seg (2 * (len sort)) & ( for i being Nat st i in Seg (2 * (len sort)) holds
S₁[i,f . i] ) ) from FINSEQ_1:sch 1(A1);
A6: rng f c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being object such that
A7: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A7;

per cases ( x is even or x is odd ) ;

suppose x is even ; :: thesis: y in NAT

then ex i being Nat st x = 2 * i by ABIAN:def 2;
then f . x = 0 by A5, A7;
hence y in NAT by A7; :: thesis: verum

end;

suppose x is odd ; :: thesis: y in NAT

then consider i being Nat such that
A8: x = (2 * i) + 1 by ABIAN:9;
(2 * (i + 1)) - 1 = x by A8;
then f . x = (g . (sort _ ((i + 1),1))) + ((((g *. sort) . (i + 1)),2) +...) by A7, A5;
hence y in NAT by A7, ORDINAL1:def 12; :: thesis: verum

end;

end;

end;

A9: len f = 2 * (len sort) by A5, FINSEQ_1:def 3;
then reconsider f = f as 2 * (len sort) -element FinSequence of NAT by A6, FINSEQ_1:def 4, CARD_1:def 7;
take f ; :: thesis: for j being Nat holds
( f . (2 * j) = 0 & f . ((2 * j) - 1) = (g . (sort _ (j,1))) + ((((g *. sort) . j),2) +...) )
let i be Nat; :: thesis: ( f . (2 * i) = 0 & f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) )
thus f . (2 * i) = 0 :: thesis: f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...)

proof

( 2 * i in dom f or not 2 * i in dom f ) ;
hence f . (2 * i) = 0 by A5, FUNCT_1:def 2; :: thesis: verum

end;

thus f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) :: thesis: verum

proof

per cases ( (2 * i) - 1 in dom f or (2 * i) - 1 > len f or (2 * i) - 1 < 1 ) by FINSEQ_3:25;

suppose (2 * i) - 1 in dom f ; :: thesis: f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...)

hence f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) by A5; :: thesis: verum

end;

suppose A10: (2 * i) - 1 > len f ; :: thesis: f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...)

then A11: not (2 * i) - 1 in dom f by FINSEQ_3:25;
((2 * i) - 1) + 1 > len f by A10, NAT_1:13;
then i > len sort by A9, XREAL_1:64;
then A12: not i in dom sort by FINSEQ_3:25;
then sort . i = {} by FUNCT_1:def 2;
then not sort _ (i,1) in dom g by FINSEQ_3:25;
then A13: g . (sort _ (i,1)) = {} by FUNCT_1:def 2;
dom (g *. sort) = dom sort by FOMODEL2:def 6;
then (g *. sort) . i = {} by A12, FUNCT_1:def 2;
then (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) = 0 by FLEXARY1:15, A13;
hence f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) by A11, FUNCT_1:def 2; :: thesis: verum

end;

suppose A14: (2 * i) - 1 < 1 ; :: thesis: f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...)

then A15: not (2 * i) - 1 in dom f by FINSEQ_3:25;
((2 * i) - 1) + 1 < 1 + 1 by A14, XREAL_1:6;
then 2 * i < 2 * 1 ;
then A16: not i in dom sort by XREAL_1:64, FINSEQ_3:25;
then sort . i = 0 by FUNCT_1:def 2;
then not sort _ (i,1) in dom g by FUNCT_1:def 2, FINSEQ_3:25;
then A17: g . (sort _ (i,1)) = 0 by FUNCT_1:def 2;
dom (g *. sort) = dom sort by FOMODEL2:def 6;
then (g *. sort) . i = {} by A16, FUNCT_1:def 2;
then (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) = 0 by FLEXARY1:15, A17;
hence f . ((2 * i) - 1) = (g . (sort _ (i,1))) + ((((g *. sort) . i),2) +...) by A15, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;