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