let D be non empty set ; 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; 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; ( 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
; 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; verum