let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st f is circular & p in rng f holds
rng (Rotate (f,p)) = rng f

let p be Element of D; :: thesis: for f being FinSequence of D st f is circular & p in rng f holds
rng (Rotate (f,p)) = rng f

let f be FinSequence of D; :: thesis: ( f is circular & p in rng f implies rng (Rotate (f,p)) = rng f )
assume that
A1: f is circular and
A2: p in rng f ; :: thesis: rng (Rotate (f,p)) = rng f
A3: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by ;
A4: rng ((f -: p) /^ 1) c= rng (f -: p) by FINSEQ_5:33;
rng (f -: p) c= rng f by FINSEQ_5:48;
then A5: rng ((f -: p) /^ 1) c= rng f by A4;
A6: rng ((f :- p) ^ ((f -: p) /^ 1)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31;
rng (f :- p) c= rng f by ;
hence rng (Rotate (f,p)) c= rng f by ; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (Rotate (f,p))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in rng (Rotate (f,p)) )
assume x in rng f ; :: thesis: x in rng (Rotate (f,p))
then consider i being Nat such that
A7: i in dom f and
A8: f . i = x by FINSEQ_2:10;
A9: x = f /. i by ;
per cases ( i = 1 or ( i <= p .. f & i <> 1 ) or i > p .. f ) ;
suppose A10: i = 1 ; :: thesis: x in rng (Rotate (f,p))
len (f :- p) = len (<*p*> ^ (f /^ (p .. f))) by FINSEQ_5:def 2
.= () + (len (f /^ (p .. f))) by FINSEQ_1:22
.= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ;
then 1 <= len (f :- p) by NAT_1:11;
then A11: len (f :- p) in dom (f :- p) by FINSEQ_3:25;
x = (f :- p) /. (len (f :- p)) by ;
then x in rng (f :- p) by ;
hence x in rng (Rotate (f,p)) by ; :: thesis: verum
end;
suppose that A12: i <= p .. f and
A13: i <> 1 ; :: thesis: x in rng (Rotate (f,p))
A14: i <> 0 by ;
then A15: i > 0 + 1 by ;
then A16: i in Seg (p .. f) by A12;
consider j being Nat such that
A17: i = j + 1 by ;
A18: j >= 1 by ;
A19: i <= len (f -: p) by ;
then 1 <= len (f -: p) by ;
then len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 1;
then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ;
then j <= len ((f -: p) /^ 1) by ;
then A20: j in dom ((f -: p) /^ 1) by ;
A21: len <*((f -: p) /. 1)*> = 1 by FINSEQ_1:39;
f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by ;
then ((f -: p) /^ 1) /. j = (f -: p) /. i by
.= f /. i by ;
then x in rng ((f -: p) /^ 1) by ;
hence x in rng (Rotate (f,p)) by ; :: thesis: verum
end;
suppose i > p .. f ; :: thesis: x in rng (Rotate (f,p))
then reconsider j = i - (p .. f) as Element of NAT by INT_1:5;
A22: j + 1 >= 1 by NAT_1:11;
i <= len f by ;
then A23: j <= (len f) - (p .. f) by XREAL_1:9;
len (f :- p) = ((len f) - (p .. f)) + 1 by ;
then j + 1 <= len (f :- p) by ;
then A24: j + 1 in dom (f :- p) by ;
j + (p .. f) = i ;
then f /. i = (f :- p) /. (j + 1) by ;
then x in rng (f :- p) by ;
hence x in rng (Rotate (f,p)) by ; :: thesis: verum
end;
end;