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))

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

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

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;

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 ) ;

suppose that A6: x .. f < p .. f and
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;

suppose that A13: x .. f < p .. f and
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;

suppose x .. f >= p .. f ; :: thesis: x in rng (Rotate (f,p))

then x in rng (f :- p) by A1, A3, A4, Th62;
hence x in rng (Rotate (f,p)) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

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

then Rotate (f,p) = f by Def2;
hence rng (f /^ 1) c= rng (Rotate (f,p)) by FINSEQ_5:33; :: thesis: verum

end;

end;