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:11;
( 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:8; :: thesis: verum