take p = <*{}*>; :: thesis: ( len p > 0 & ( for i being Element of 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 Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in R
let i be Element of 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:4, FINSEQ_1:55;
then i = 1 by A1, TARSKI:def 1;
hence [(p . i),(p . (i + 1))] in R by A3, A2, TARSKI:def 1; :: thesis: verum