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