let n be Nat; :: thesis: for f being FinSequence of REAL st n in dom f holds
len (f | n) = n
let f be FinSequence of REAL ; :: 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