:: deftheorem defines Prefix FIB_NUM2:def 1 :
for f being sequence of NAT
for A being finite with_non-empty_elements natural-membered set holds Prefix (f,A) = Seq (f | A);