let p be FinSequence; :: thesis: for i being Nat holds
( not i in dom p or i = len p or i < len p )
let i be Nat; :: thesis: ( not i in dom p or i = len p or i < len p )
assume i in dom p ; :: thesis: ( i = len p or i < len p )
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 = len p or i < len p ) by XXREAL_0:1; :: thesis: verum