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