let R be Relation; for a, b being object st [a,b] in R holds
<*a,b*> is RedSequence of R
let a, b be object ; ( [a,b] in R implies <*a,b*> is RedSequence of R )
assume A1:
[a,b] in R
; <*a,b*> is RedSequence of R
set p = <*a,b*>;
thus
len <*a,b*> > 0
; REWRITE1:def 2 for i being Nat st i in dom <*a,b*> & i + 1 in dom <*a,b*> holds
[(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
let i be Nat; ( i in dom <*a,b*> & i + 1 in dom <*a,b*> implies [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R )
assume that
A2:
i in dom <*a,b*>
and
A3:
i + 1 in dom <*a,b*>
; [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
len <*a,b*> = 1 + 1
by FINSEQ_1:44;
then
i + 1 <= 1 + 1
by A3, Lm1;
then A4:
i <= 1
by XREAL_1:6;
i >= 1
by A2, Lm1;
then
( <*a,b*> . 1 = a & i = 1 )
by A4, FINSEQ_1:44, XXREAL_0:1;
hence
[(<*a,b*> . i),(<*a,b*> . (i + 1))] in R
by A1, FINSEQ_1:44; verum