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 ;
p .. f <> 1 by ;
then p .. f > 1 by ;
then p .. f = (p .. (f /^ 1)) + 1 by ;
then A9: (x .. (f /^ 1)) + 1 >= p .. f by ;
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 ;
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 ;
then A12: (x .. (f /^ 1)) + 1 <= len f by ;
q = (f /^ 1) /. (q .. (f /^ 1)) by
.= f /. ((q .. (f /^ 1)) + 1) by ;
then x in rng (f :- p) by A1, A12, A9, Th63;
hence x in rng (Rotate (f,p)) by ; :: 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 ;
p .. f >= 1 by ;
then p .. f > 1 by ;
then p in rng (f /^ 1) by ;
then x in rng ((f /^ 1) -: p) by ;
then x in rng ((f -: p) /^ 1) by ;
hence x in rng (Rotate (f,p)) by ; :: 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 ; :: 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;