let k be Element of NAT ; :: thesis: for D being non empty set ex p being XFinSequence of st len p = k
let D be non empty set ; :: thesis: ex p being XFinSequence of st len p = k
consider y being Element of D;
set p = k --> y;
( dom (k --> y) = k & ( for n being Element of NAT st n in k holds
(k --> y) . n = y ) ) by FUNCOP_1:13, FUNCOP_1:19;
then reconsider p = k --> y as XFinSequence by Th7;
A2: rng p c= {y} by FUNCOP_1:19;
{y} c= D by ZFMISC_1:37;
then rng p c= D by A2, XBOOLE_1:1;
then reconsider p = p as XFinSequence of by RELAT_1:def 19;
take p ; :: thesis: len p = k
thus len p = k by FUNCOP_1:19; :: thesis: verum