let m be non zero Nat; :: thesis: for k being Nat
for X being non-empty m -element FinSequence st k <= m holds
X | k is non-empty b₁ -element FinSequence
let k be Nat; :: thesis: for X being non-empty m -element FinSequence st k <= m holds
X | k is non-empty k -element FinSequence
let X be non-empty m -element FinSequence; :: thesis: ( k <= m implies X | k is non-empty k -element FinSequence )
assume A1: k <= m ; :: thesis: X | k is non-empty k -element FinSequence
len X = m by CARD_1:def 7;
then len (X | k) = k by FINSEQ_1:59, A1;
hence X | k is non-empty k -element FinSequence by CARD_1:def 7; :: thesis: verum