reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
n9 |-> a is FinSequence of K ;
hence n |-> a is FinSequence of K ; :: thesis: verum