:: deftheorem defines Expand NUMBER18:def 11 :
for s, m, a being non zero Nat
for f being b₁ -element natural-valued positive-yielding FinSequence holds Expand (f,m,a) = (f | (s -' 1)) ^ ((a |^ m) |-> (a * (f . s)));