take p = <*{}*>; :: thesis: ( len p > 0 & ( for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R ) )
thus len p > 0 ; :: thesis: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R
let i be Nat; :: thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in R )
assume that
A1: i in dom p and
A2: i + 1 in dom p ; :: thesis: [(p . i),(p . (i + 1))] in R
A3: dom p = {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by A1, TARSKI:def 1;
hence [(p . i),(p . (i + 1))] in R by A3, A2, TARSKI:def 1; :: thesis: verum