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 ) )
A1: ( dom p = {1} & len p = 1 ) by FINSEQ_1:4, FINSEQ_1:55, FINSEQ_1:57;
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 ( i in dom p & i + 1 in dom p ) ; :: thesis: [(p . i),(p . (i + 1))] in R
then ( i = 1 & i + 1 = 1 ) by A1, TARSKI:def 1;
hence [(p . i),(p . (i + 1))] in R ; :: thesis: verum