let f be FinSequence; :: thesis: for i being Nat holds
( not i + 1 in dom f or i in dom f or i = 0 )
let i be Nat; :: thesis: ( not i + 1 in dom f or i in dom f or i = 0 )
assume A1: i + 1 in dom f ; :: thesis: ( i in dom f or i = 0 )
then 1 <= i + 1 by FINSEQ_3:25;
then A2: ( 1 < i + 1 or 1 + 0 = i + 1 ) by XXREAL_0:1;

per cases ( i = 0 or 1 <= i ) by A2, NAT_1:13;

suppose i = 0 ; :: thesis: ( i in dom f or i = 0 )

hence ( i in dom f or i = 0 ) ; :: thesis: verum

end;

suppose A3: 1 <= i ; :: thesis: ( i in dom f or i = 0 )

i + 1 <= len f by A1, FINSEQ_3:25;
then i <= len f by NAT_1:13;
hence ( i in dom f or i = 0 ) by A3, FINSEQ_3:25; :: thesis: verum

end;

end;