let D be set ; :: thesis: for p being FinSequence of D st dom p <> {} holds
1 in dom p
let p be FinSequence of D; :: thesis: ( dom p <> {} implies 1 in dom p )
assume A1: dom p <> {} ; :: thesis: 1 in dom p
consider l being Nat such that
A2: dom p = Seg l by FINSEQ_1:def 2;
1 <= l by A1, A2, FINSEQ_1:4, NAT_1:14;
hence 1 in dom p by A2, FINSEQ_1:3; :: thesis: verum