let R be Relation; :: thesis: for a, b being object st [a,b] in R holds
<*a,b*> is RedSequence of R
let a, b be object ; :: thesis: ( [a,b] in R implies <*a,b*> is RedSequence of R )
assume A1: [a,b] in R ; :: thesis: <*a,b*> is RedSequence of R
set p = <*a,b*>;
thus len <*a,b*> > 0 ; :: according to REWRITE1:def 2 :: thesis: 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; :: thesis: ( 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*> ; :: thesis: [(<*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, XXREAL_0:1;
hence [(<*a,b*> . i),(<*a,b*> . (i + 1))] in R by A1; :: thesis: verum