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