theorem Expand0: :: NUMBER18:72

for s, m being Nat
for f being b₁ -element natural-valued positive-yielding FinSequence st s = 2 |^ m & f = s |-> 2 holds
f is m -solution_of_Sierp167