let p be FinSequence; :: thesis: for i being Nat holds
( not i in dom p or i = 1 or 1 < i )
let i be Nat; :: thesis: ( not i in dom p or i = 1 or 1 < i )
assume i in dom p ; :: thesis: ( i = 1 or 1 < i )
then i in Seg (len p) by FINSEQ_1:def 3;
then not not i = 1 & ... & not i = len p by FINSEQ_1:91;
hence ( i = 1 or 1 < i ) by XXREAL_0:1; :: thesis: verum