theorem :: FLEXARY1:31

for n being Nat ex f being natural-valued increasing FinSequence st n = ((2 |^ f) . 1) + (((2 |^ f),2) +...)