let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))

let p be Element of D; :: thesis: for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))

let f be FinSequence of D; :: thesis: rng (f /^ 1) c= rng (Rotate (f,p))

for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))

let p be Element of D; :: thesis: for f being FinSequence of D holds rng (f /^ 1) c= rng (Rotate (f,p))

let f be FinSequence of D; :: thesis: rng (f /^ 1) c= rng (Rotate (f,p))

per cases
( p in rng f or not p in rng f )
;

end;

suppose A1:
p in rng f
; :: thesis: rng (f /^ 1) c= rng (Rotate (f,p))

then
Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1)
by Def2;

then A2: rng (Rotate (f,p)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31;

thus rng (f /^ 1) c= rng (Rotate (f,p)) :: thesis: verum

end;then A2: rng (Rotate (f,p)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31;

thus rng (f /^ 1) c= rng (Rotate (f,p)) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f /^ 1) or x in rng (Rotate (f,p)) )

assume A3: x in rng (f /^ 1) ; :: thesis: x in rng (Rotate (f,p))

A4: rng (f /^ 1) c= rng f by FINSEQ_5:33;

then A5: x in rng f by A3;

end;assume A3: x in rng (f /^ 1) ; :: thesis: x in rng (Rotate (f,p))

A4: rng (f /^ 1) c= rng f by FINSEQ_5:33;

then A5: x in rng f by A3;

per cases
( ( x .. f < p .. f & x .. (f /^ 1) >= p .. (f /^ 1) ) or ( x .. f < p .. f & x .. (f /^ 1) <= p .. (f /^ 1) ) or x .. f >= p .. f )
;

end;

suppose that A6:
x .. f < p .. f
and

A7: x .. (f /^ 1) >= p .. (f /^ 1) ; :: thesis: x in rng (Rotate (f,p))

A7: x .. (f /^ 1) >= p .. (f /^ 1) ; :: thesis: x in rng (Rotate (f,p))

A8:
p .. f >= 1
by A1, FINSEQ_4:21;

p .. f <> 1 by A3, A4, A6, FINSEQ_4:21;

then p .. f > 1 by A8, XXREAL_0:1;

then p .. f = (p .. (f /^ 1)) + 1 by A1, Th56;

then A9: (x .. (f /^ 1)) + 1 >= p .. f by A7, XREAL_1:6;

rng f c= D by FINSEQ_1:def 4;

then reconsider q = x as Element of D by A5;

A10: x .. (f /^ 1) in dom (f /^ 1) by A3, FINSEQ_4:20;

f <> {} by A1;

then len f >= 1 by NAT_1:14;

then (len f) - 1 = len (f /^ 1) by RFINSEQ:def 1;

then A11: len f = (len (f /^ 1)) + 1 ;

x .. (f /^ 1) <= len (f /^ 1) by A3, FINSEQ_4:21;

then A12: (x .. (f /^ 1)) + 1 <= len f by A11, XREAL_1:6;

q = (f /^ 1) /. (q .. (f /^ 1)) by A3, FINSEQ_5:38

.= f /. ((q .. (f /^ 1)) + 1) by A10, FINSEQ_5:27 ;

then x in rng (f :- p) by A1, A12, A9, Th63;

hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;p .. f <> 1 by A3, A4, A6, FINSEQ_4:21;

then p .. f > 1 by A8, XXREAL_0:1;

then p .. f = (p .. (f /^ 1)) + 1 by A1, Th56;

then A9: (x .. (f /^ 1)) + 1 >= p .. f by A7, XREAL_1:6;

rng f c= D by FINSEQ_1:def 4;

then reconsider q = x as Element of D by A5;

A10: x .. (f /^ 1) in dom (f /^ 1) by A3, FINSEQ_4:20;

f <> {} by A1;

then len f >= 1 by NAT_1:14;

then (len f) - 1 = len (f /^ 1) by RFINSEQ:def 1;

then A11: len f = (len (f /^ 1)) + 1 ;

x .. (f /^ 1) <= len (f /^ 1) by A3, FINSEQ_4:21;

then A12: (x .. (f /^ 1)) + 1 <= len f by A11, XREAL_1:6;

q = (f /^ 1) /. (q .. (f /^ 1)) by A3, FINSEQ_5:38

.= f /. ((q .. (f /^ 1)) + 1) by A10, FINSEQ_5:27 ;

then x in rng (f :- p) by A1, A12, A9, Th63;

hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def 3; :: thesis: verum

suppose that A13:
x .. f < p .. f
and

A14: x .. (f /^ 1) <= p .. (f /^ 1) ; :: thesis: x in rng (Rotate (f,p))

A14: x .. (f /^ 1) <= p .. (f /^ 1) ; :: thesis: x in rng (Rotate (f,p))

A15:
p .. f <> 1
by A3, A4, A13, FINSEQ_4:21;

p .. f >= 1 by A1, FINSEQ_4:21;

then p .. f > 1 by A15, XXREAL_0:1;

then p in rng (f /^ 1) by A1, Th57;

then x in rng ((f /^ 1) -: p) by A3, A14, FINSEQ_5:46;

then x in rng ((f -: p) /^ 1) by A1, A15, Th60;

hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;p .. f >= 1 by A1, FINSEQ_4:21;

then p .. f > 1 by A15, XXREAL_0:1;

then p in rng (f /^ 1) by A1, Th57;

then x in rng ((f /^ 1) -: p) by A3, A14, FINSEQ_5:46;

then x in rng ((f -: p) /^ 1) by A1, A15, Th60;

hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def 3; :: thesis: verum