let D be non empty set ; :: thesis: for f being FinSequence of D
for p, q being Element of D st p in rng f & q in rng f & p .. f <= q .. f holds
q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1
let f be FinSequence of D; :: thesis: for p, q being Element of D st p in rng f & q in rng f & p .. f <= q .. f holds
q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1
let p, q be Element of D; :: thesis: ( p in rng f & q in rng f & p .. f <= q .. f implies q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1 )
assume that
A1: p in rng f and
A2: q in rng f ; :: thesis: ( not p .. f <= q .. f or q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1 )
A3: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, FINSEQ_6:def 2;
assume A4: p .. f <= q .. f ; :: thesis: q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1
then q in rng (f :- p) by A1, A2, FINSEQ_6:62;
hence q .. (Rotate (f,p)) = q .. (f :- p) by A3, FINSEQ_6:6
.= ((q .. f) - (p .. f)) + 1 by A1, A2, A4, Th2 ;
:: thesis: verum