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;
reconsider p = p as XFinSequence of D ;
take p ; :: thesis: len p = k
thus len p = k by FUNCOP_1:19; :: thesis: verum