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

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