let R be Relation; :: thesis: for p being RedSequence of R holds Rev p is RedSequence of R ~
let p be RedSequence of R; :: thesis: Rev p is RedSequence of R ~
len p > 0 ;
hence len (Rev p) > 0 by FINSEQ_5:def 3; :: according to REWRITE1:def 2 :: thesis: for i being Nat st i in dom (Rev p) & i + 1 in dom (Rev p) holds
[((Rev p) . i),((Rev p) . (i + 1))] in R ~
let i be Nat; :: thesis: ( i in dom (Rev p) & i + 1 in dom (Rev p) implies [((Rev p) . i),((Rev p) . (i + 1))] in R ~ )
assume that
A1: i in dom (Rev p) and
A2: i + 1 in dom (Rev p) ; :: thesis: [((Rev p) . i),((Rev p) . (i + 1))] in R ~
A3: len (Rev p) = len p by FINSEQ_5:def 3;
then A4: dom (Rev p) = Seg (len p) by FINSEQ_1:def 3;
i + 1 <= len p by A3, A2, Lm1;
then reconsider k = ((len p) - (i + 1)) + 1 as Nat by FINSEQ_5:1;
A5: dom p = Seg (len p) by FINSEQ_1:def 3;
then A6: k in dom p by A4, A2, FINSEQ_5:2;
k = (len p) - i ;
then k + 1 in dom p by A4, A5, A1, FINSEQ_5:2;
then A7: [(p . k),(p . (k + 1))] in R by A6, Def2;
( (Rev p) . i = p . (((len p) - i) + 1) & (Rev p) . (i + 1) = p . (((len p) - (i + 1)) + 1) ) by A1, A2, FINSEQ_5:def 3;
hence [((Rev p) . i),((Rev p) . (i + 1))] in R ~ by A7, RELAT_1:def 7; :: thesis: verum