let n be Nat; :: thesis: ex f being natural-valued increasing FinSequence st n = ((2 |^ f) . 1) + (((2 |^ f),2) +...)
set D = digits (n,2);
consider d being XFinSequence of NAT such that
A1: ( dom d = dom (digits (n,2)) & ( for i being Nat st i in dom d holds
d . i = ((digits (n,2)) . i) * (2 |^ i) ) & value ((digits (n,2)),2) = Sum d ) by NUMERAL1:def 1;
defpred S₁[ Nat] means ( $1 <= len d implies ex f being natural-valued increasing FinSequence st
( ( len f = 0 or f . (len f) < $1 ) & Sum (2 |^ f) = Sum (d | $1) ) );
A2: S₁[ 0 ]

proof

assume 0 <= len d ; :: thesis: ex f being natural-valued increasing FinSequence st
( ( len f = 0 or f . (len f) < 0 ) & Sum (2 |^ f) = Sum (d | 0) )
reconsider f = <*> NAT as natural-valued increasing FinSequence ;
take f ; :: thesis: ( ( len f = 0 or f . (len f) < 0 ) & Sum (2 |^ f) = Sum (d | 0) )
Sum (2 |^ f) = 0 by RVSUM_1:72;
hence ( ( len f = 0 or f . (len f) < 0 ) & Sum (2 |^ f) = Sum (d | 0) ) ; :: thesis: verum

end;

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

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
assume A5: i + 1 <= len d ; :: thesis: ex f being natural-valued increasing FinSequence st
( ( len f = 0 or f . (len f) < i + 1 ) & Sum (2 |^ f) = Sum (d | (i + 1)) )
then consider f being natural-valued increasing FinSequence such that
A6: ( ( len f = 0 or f . (len f) < i ) & Sum (2 |^ f) = Sum (d | i) ) by NAT_1:13, A4;
A7: i in dom d by A5, NAT_1:13, AFINSQ_1:86;
then A8: ( Sum (d | (i + 1)) = (Sum (d | i)) + (d . i) & d . i = ((digits (n,2)) . i) * (2 |^ i) ) by A1, AFINSQ_2:65;
A9: ( (digits (n,2)) . i = 0 or (digits (n,2)) . i = 1 )

proof

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ( (digits (n,2)) . i = 0 or (digits (n,2)) . i = 1 )

then A10: digits (n,2) = <%0%> by NUMERAL1:def 2;
then ( dom (digits (n,2)) = 1 & 1 = Segm 1 ) by AFINSQ_1:def 4, ORDINAL1:def 17;
then i < 1 by A5, NAT_1:13, A1;
then i = 0 by NAT_1:25;
hence ( (digits (n,2)) . i = 0 or (digits (n,2)) . i = 1 ) by A10; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: ( (digits (n,2)) . i = 0 or (digits (n,2)) . i = 1 )

then ( 0 <= (digits (n,2)) . i & (digits (n,2)) . i < 2 ) by A7, A1, NUMERAL1:def 2;
hence ( (digits (n,2)) . i = 0 or (digits (n,2)) . i = 1 ) by NAT_1:23; :: thesis: verum

end;

end;

end;

per cases ( (digits (n,2)) . i = 0 or (digits (n,2)) . i = 1 ) by A9;

suppose A11: (digits (n,2)) . i = 0 ; :: thesis: ex f being natural-valued increasing FinSequence st
( ( len f = 0 or f . (len f) < i + 1 ) & Sum (2 |^ f) = Sum (d | (i + 1)) )

take f ; :: thesis: ( ( len f = 0 or f . (len f) < i + 1 ) & Sum (2 |^ f) = Sum (d | (i + 1)) )
thus ( ( len f = 0 or f . (len f) < i + 1 ) & Sum (2 |^ f) = Sum (d | (i + 1)) ) by A11, A8, A6, NAT_1:13; :: thesis: verum

end;

suppose A12: (digits (n,2)) . i = 1 ; :: thesis: ex f being natural-valued increasing FinSequence st
( ( len f = 0 or f . (len f) < i + 1 ) & Sum (2 |^ f) = Sum (d | (i + 1)) )

set fi = f ^ <*i*>;
A13: len (f ^ <*i*>) = (len f) + 1 by FINSEQ_2:16;
for e1, e2 being ExtReal st e1 in dom (f ^ <*i*>) & e2 in dom (f ^ <*i*>) & e1 < e2 holds
(f ^ <*i*>) . e1 < (f ^ <*i*>) . e2

proof

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (f ^ <*i*>) & e2 in dom (f ^ <*i*>) & e1 < e2 implies (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2 )
assume A14: ( e1 in dom (f ^ <*i*>) & e2 in dom (f ^ <*i*>) & e1 < e2 ) ; :: thesis: (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2
A15: ( 1 <= e1 & 1 <= e2 & e1 <= (len f) + 1 & e2 <= (len f) + 1 ) by A14, A13, FINSEQ_3:25;

per cases ( ( e1 <= len f & e2 <= len f ) or ( e1 <= len f & e2 > len f ) or ( e1 > len f & e2 <= len f ) or ( e1 > len f & e2 > len f ) ) ;

suppose ( e1 <= len f & e2 <= len f ) ; :: thesis: (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2

then ( e1 in dom f & e2 in dom f ) by A15, A14, FINSEQ_3:25;
then ( f . e1 < f . e2 & f . e1 = (f ^ <*i*>) . e1 & f . e2 = (f ^ <*i*>) . e2 ) by A14, VALUED_0:def 13, FINSEQ_1:def 7;
hence (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2 ; :: thesis: verum

end;

suppose A16: ( e1 <= len f & e2 > len f ) ; :: thesis: (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2

then e2 >= (len f) + 1 by A14, NAT_1:13;
then e2 = (len f) + 1 by A15, XXREAL_0:1;
then A17: (f ^ <*i*>) . e2 = i by FINSEQ_1:42;
A18: ( e1 = len f or e1 < len f ) by A16, XXREAL_0:1;
len f >= 1 by A16, A15, XXREAL_0:2;
then A19: ( f . (len f) < i & len f in dom f & e1 in dom f ) by A14, A15, A16, A6, FINSEQ_3:25;
then f . e1 <= f . (len f) by A18, VALUED_0:def 13;
then f . e1 < i by A16, A14, FINSEQ_3:25, XXREAL_0:2, A6;
hence (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2 by A19, FINSEQ_1:def 7, A17; :: thesis: verum

end;

suppose ( e1 > len f & e2 <= len f ) ; :: thesis: (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2

hence (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2 by A14, XXREAL_0:2; :: thesis: verum

end;

suppose ( e1 > len f & e2 > len f ) ; :: thesis: (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2

then ( e1 >= (len f) + 1 & e2 >= (len f) + 1 ) by A14, NAT_1:13;
hence (f ^ <*i*>) . e1 < (f ^ <*i*>) . e2 by A15, A14, XXREAL_0:1; :: thesis: verum

end;

end;

end;

then reconsider fi = f ^ <*i*> as natural-valued increasing FinSequence by VALUED_0:def 13;
take fi ; :: thesis: ( ( len fi = 0 or fi . (len fi) < i + 1 ) & Sum (2 |^ fi) = Sum (d | (i + 1)) )
( fi . (len fi) = i & i < i + 1 ) by A13, NAT_1:13, FINSEQ_1:42;
hence ( len fi = 0 or fi . (len fi) < i + 1 ) ; :: thesis: Sum (2 |^ fi) = Sum (d | (i + 1))
dom f = Seg (len f) by FINSEQ_1:def 3;
then fi | (len f) = f by FINSEQ_1:21;
then Sum (2 |^ fi) = (Sum (2 |^ f)) + (2 |^ (fi . ((len f) + 1))) by FINSEQ_2:16, Lm5;
hence Sum (2 |^ fi) = Sum (d | (i + 1)) by FINSEQ_1:42, A12, A8, A6; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
then consider f being natural-valued increasing FinSequence such that
( len f = 0 or f . (len f) < len d ) and
A20: Sum (2 |^ f) = Sum (d | (len d)) ;
A21: Sum (2 |^ f) = ((2 |^ f) . 1) + (((2 |^ f),2) +...) by Th22;
Sum d = n by A1, NUMERAL1:5;
hence ex f being natural-valued increasing FinSequence st n = ((2 |^ f) . 1) + (((2 |^ f),2) +...) by A20, A21; :: thesis: verum