A1: rng f c= NAT by VALUED_0:def 6;
{1} c= NAT by ZFMISC_1:31;
then reconsider D = (rng f) \/ {1} as non empty finite Subset of NAT by A1, XBOOLE_1:8;
set m = max D;
deffunc H1( Nat) -> Element of omega = (2 * $1) -' 1;
consider g being FinSequence of NAT such that
A2: ( len g = (max D) + 1 & ( for j being Nat st j in dom g holds
g . j = H1(j) ) ) from FINSEQ_2:sch 1();
 reconsider g = g as non empty FinSequence of NAT by A2;
rng f c= rng g
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in rng g )
assume A3: y in rng f ; :: thesis: y in rng g
then consider x being object such that
A4: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider n = y as odd Nat by A4, Def2;
consider i being Nat such that
A5: (2 * i) + 1 = n by ABIAN:9;
n in D by A3, XBOOLE_0:def 3;
then A6: n <= max D by XXREAL_2:def 8;
( max D <= (max D) + ((max D) + 1) & (max D) + ((max D) + 1) = (2 * (max D)) + 1 ) by NAT_1:11;
then (2 * i) + 1 <= (2 * (max D)) + 1 by A6, A5, XXREAL_0:2;
then 2 * i <= 2 * (max D) by XREAL_1:6;
then i <= max D by XREAL_1:68;
then A7: ( 1 <= i + 1 & i + 1 <= (max D) + 1 ) by XREAL_1:6, NAT_1:11;
then A8: i + 1 in dom g by A2, FINSEQ_3:25;
A9: g . (i + 1) = (2 * (i + 1)) -' 1 by A7, A2, FINSEQ_3:25;
2 * 1 <= 2 * (i + 1) by NAT_1:11, XREAL_1:64;
then g . (i + 1) = (2 * (i + 1)) - 1 by XXREAL_0:2, A9, XREAL_1:233;
hence y in rng g by A5, A8, FUNCT_1:def 3; :: thesis: verum
end;
then consider o being len g -element DoubleReorganization of dom f such that
A10: for n being Nat holds
( o . n is increasing & g . n = f . (o _ (n,1)) & ... & g . n = f . (o _ (n,(len (o . n)))) ) by FLEXARY1:39;
o is valued_reorganization of f
proof
thus for n being Nat ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n)))) :: according to FLEXARY1:def 9 :: thesis: for b1, b2, b3, b4 being set holds
( not b3 in dom (o . b1) or not b4 in dom (o . b2) or not f . (o _ (b1,b3)) = f . (o _ (b2,b4)) or b1 = b2 )
proof
let n be Nat; :: thesis: ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n))))
g . n = f . (o _ (n,1)) & ... & g . n = f . (o _ (n,(len (o . n)))) by A10;
hence ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n)))) ; :: thesis: verum
end;
let n1, n2, i1, i2 be Nat; :: thesis: ( not i1 in dom (o . n1) or not i2 in dom (o . n2) or not f . (o _ (n1,i1)) = f . (o _ (n2,i2)) or n1 = n2 )
assume A11: ( i1 in dom (o . n1) & i2 in dom (o . n2) & f . (o _ (n1,i1)) = f . (o _ (n2,i2)) ) ; :: thesis: n1 = n2
A12: g . n1 = f . (o _ (n1,1)) & ... & g . n1 = f . (o _ (n1,(len (o . n1)))) by A10;
( 1 <= i1 & i1 <= len (o . n1) ) by A11, FINSEQ_3:25;
then A13: g . n1 = f . (o _ (n1,i1)) by A12;
A14: g . n2 = f . (o _ (n2,1)) & ... & g . n2 = f . (o _ (n2,(len (o . n2)))) by A10;
( 1 <= i2 & i2 <= len (o . n2) ) by A11, FINSEQ_3:25;
then A15: g . n1 = g . n2 by A14, A11, A13;
len o = len g by CARD_1:def 7;
then A16: dom o = dom g by FINSEQ_3:29;
A17: n1 in dom g
proof
assume not n1 in dom g ; :: thesis: contradiction
then o . n1 = {} by A16, FUNCT_1:def 2;
hence contradiction by A11; :: thesis: verum
end;
then A18: g . n1 = H1(n1) by A2;
A19: n2 in dom g
proof
assume not n2 in dom g ; :: thesis: contradiction
then o . n2 = {} by A16, FUNCT_1:def 2;
hence contradiction by A11; :: thesis: verum
end;
then A20: H1(n1) = H1(n2) by A2, A18, A15;
2 * 1 <= 2 * n1 by A17, FINSEQ_3:25, XREAL_1:64;
then A21: (2 * n1) -' 1 = (2 * n1) - 1 by XXREAL_0:2, XREAL_1:233;
2 * 1 <= 2 * n2 by A19, FINSEQ_3:25, XREAL_1:64;
then (2 * n2) -' 1 = (2 * n2) - 1 by XXREAL_0:2, XREAL_1:233;
hence n1 = n2 by A20, A21; :: thesis: verum
end;
then reconsider o = o as valued_reorganization of f ;
take o ; :: thesis: for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n))))
for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n))))
proof
let n, i be Nat; :: thesis: ( not 1 <= i or not i <= len (o . n) or (2 * n) - 1 = f . (o _ (n,i)) )
assume A22: ( 1 <= i & i <= len (o . n) ) ; :: thesis: (2 * n) - 1 = f . (o _ (n,i))
A23: g . n = f . (o _ (n,1)) & ... & g . n = f . (o _ (n,(len (o . n)))) by A10;
len o = len g by CARD_1:def 7;
then A24: dom o = dom g by FINSEQ_3:29;
o . n <> {} by A22;
then n in dom o by FUNCT_1:def 2;
then A25: ( 1 <= n & n <= len o & g . n = H1(n) ) by A24, A2, FINSEQ_3:25;
then 2 * 1 <= 2 * n by XREAL_1:64;
then (2 * n) -' 1 = (2 * n) - 1 by XXREAL_0:2, XREAL_1:233;
hence (2 * n) - 1 = f . (o _ (n,i)) by A23, A22, A25; :: thesis: verum
end;
hence for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ; :: thesis: verum