let n be Nat; :: thesis: for f being FinSequence holds
( n in dom f iff ( n <> 0 & n <= len f ) )
let f be FinSequence; :: thesis: ( n in dom f iff ( n <> 0 & n <= len f ) )
( n in dom f iff ( n >= 1 & n <= len f ) ) by FINSEQ_3:25;
hence ( n in dom f iff ( n <> 0 & n <= len f ) ) by NAT_1:14; :: thesis: verum