let a be natural Number ; :: thesis: for D being non empty set ex p being FinSequence of D st len p = a
let D be non empty set ; :: thesis: ex p being FinSequence of D st len p = a
reconsider a = a as Element of NAT by ORDINAL1:def 12;
set y = the Element of D;
set p = (Seg a) --> the Element of D;
A1: dom ((Seg a) --> the Element of D) = Seg a by FUNCOP_1:13;
then reconsider p = (Seg a) --> the Element of D as FinSequence by Def2;
( rng p c= { the Element of D} & { the Element of D} c= D ) by FUNCOP_1:13, ZFMISC_1:31;
then reconsider q = p as FinSequence of D by Def4, XBOOLE_1:1;
take q ; :: thesis: len q = a
thus len q = a by A1, Def3; :: thesis: verum