let n be Nat; :: thesis: for D being set
for f being b₁ -valued FinSequence st n in dom f holds
len (f | n) = n
let D be set ; :: thesis: for f being D -valued FinSequence st n in dom f holds
len (f | n) = n
let f be D -valued FinSequence; :: thesis: ( n in dom f implies len (f | n) = n )
assume n in dom f ; :: thesis: len (f | n) = n
then n <= len f by FINSEQ_3:25;
hence len (f | n) = n by FINSEQ_1:59; :: thesis: verum