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
set y = the Element of D;
set p = k --> the Element of D;
reconsider p = k --> the Element of D as XFinSequence ;
reconsider p = p as XFinSequence of D ;
take p ; :: thesis: len p = k
thus len p = k ; :: thesis: verum