let k be Nat; :: thesis: for D being non empty set ex p being XFinSequence of D st len p = k
let D be non empty set ; :: thesis: ex p being XFinSequence of D st len p = k
consider y being Element of D;
set p = k --> y;
dom (k --> y) = k by FUNCOP_1:19;
then reconsider p = k --> y as XFinSequence by Th7;
( 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 p = p as XFinSequence of D by RELAT_1:def 19;
take p ; :: thesis: len p = k
thus len p = k by FUNCOP_1:19; :: thesis: verum