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 dom p <> {} ; :: thesis: 1 in dom p
then p <> {} ;
hence 1 in dom p by FINSEQ_5:6; :: thesis: verum