let p be FinSequence; :: thesis: for n being Nat holds
( n in dom p iff ( 1 <= n & n <= len p ) )
let n be Nat; :: thesis: ( n in dom p iff ( 1 <= n & n <= len p ) )
thus ( n in dom p implies ( 1 <= n & n <= len p ) ) :: thesis: ( 1 <= n & n <= len p implies n in dom p )
proof
assume n in dom p ; :: thesis: ( 1 <= n & n <= len p )
then n in Seg (len p) by FINSEQ_1:def 3;
hence ( 1 <= n & n <= len p ) by FINSEQ_1:1; :: thesis: verum
end;
assume that
A1: 1 <= n and
A2: n <= len p ; :: thesis: n in dom p
n in Seg (len p) by A1, A2, FINSEQ_1:1;
hence n in dom p by FINSEQ_1:def 3; :: thesis: verum