let a be Nat; :: 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 13;
consider y being Element of D;
set p = (Seg a) --> y;
A1: dom ((Seg a) --> y) = Seg a by FUNCOP_1:19;
then reconsider p = (Seg a) --> y as FinSequence by Def2;
( rng p c= {y} & {y} c= D ) by FUNCOP_1:19, ZFMISC_1:37;
then rng p c= D by XBOOLE_1:1;
then reconsider q = p as FinSequence of D by Def4;
take q ; :: thesis: len q = a
thus len q = a by A1, Def3; :: thesis: verum