let D be non empty set ; :: thesis: for f being FinSequence of D
for p1, p2, p3 being Element of D st p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f & p2 .. f < p3 .. f holds
p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1))
let f be FinSequence of D; :: thesis: for p1, p2, p3 being Element of D st p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f & p2 .. f < p3 .. f holds
p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1))
let p1, p2, p3 be Element of D; :: thesis: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f & p2 .. f < p3 .. f implies p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1)) )
assume that
A1: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f ) and
A2: p2 .. f < p3 .. f ; :: thesis: p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1))
A3: (p2 .. f) - (p1 .. f) < (p3 .. f) - (p1 .. f) by A2, XREAL_1:9;
( p2 .. (Rotate (f,p1)) = ((p2 .. f) - (p1 .. f)) + 1 & p3 .. (Rotate (f,p1)) = ((p3 .. f) - (p1 .. f)) + 1 ) by A1, A2, Th4, XXREAL_0:2;
hence p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1)) by A3, XREAL_1:6; :: thesis: verum