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

( 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