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