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 A2, Def2;
A4: rng ((f :- p) ^ ((f -: p) /^ 1)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:44;
A5: rng (f :- p) c= rng f by A2, FINSEQ_5:58;
A6: rng (f -: p) c= rng f by FINSEQ_5:51;
rng ((f -: p) /^ 1) c= rng (f -: p) by FINSEQ_5:36;
then rng ((f -: p) /^ 1) c= rng f by A6, XBOOLE_1:1;
hence rng (Rotate f,p) c= rng f by A3, A4, A5, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (Rotate f,p)
let x be set ; :: 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:11;
A9: x = f /. i by A7, A8, PARTFUN1:def 8;

per cases ( i = 1 or ( i <= p .. f & i <> 1 ) or i > p .. f ) ;

suppose i = 1 ; :: thesis: x in rng (Rotate f,p)

then A10: x = f /. (len f) by A1, A9, Def1
.= (f :- p) /. (len (f :- p)) by A2, FINSEQ_5:57 ;
len (f :- p) = len (<*p*> ^ (f /^ (p .. f))) by FINSEQ_5:def 2
.= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:35
.= 1 + (len (f /^ (p .. f))) by FINSEQ_1:56 ;
then 1 <= len (f :- p) by NAT_1:11;
then len (f :- p) in dom (f :- p) by FINSEQ_3:27;
then x in rng (f :- p) by A10, PARTFUN2:4;
hence x in rng (Rotate f,p) by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose that A11: i <= p .. f and
A12: i <> 1 ; :: thesis: x in rng (Rotate f,p)

A13: i <> 0 by A7, FINSEQ_3:27;
then A14: i > 0 + 1 by A12, NAT_1:26;
consider j being Nat such that
A15: i = j + 1 by A13, NAT_1:6;
A16: i <= len (f -: p) by A2, A11, FINSEQ_5:45;
then 1 <= len (f -: p) by A13, NAT_1:26, XXREAL_0:2;
then len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 2;
then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ;
then A17: j <= len ((f -: p) /^ 1) by A15, A16, XREAL_1:8;
j >= 1 by A14, A15, NAT_1:14;
then A18: j in dom ((f -: p) /^ 1) by A17, FINSEQ_3:27;
A19: len <*((f -: p) /. 1)*> = 1 by FINSEQ_1:56;
A20: i in Seg (p .. f) by A11, A14, FINSEQ_1:3;
f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by A2, FINSEQ_5:32, FINSEQ_5:50;
then ((f -: p) /^ 1) /. j = (f -: p) /. i by A15, A18, A19, FINSEQ_4:84
.= f /. i by A2, A20, FINSEQ_5:46 ;
then x in rng ((f -: p) /^ 1) by A9, A18, PARTFUN2:4;
hence x in rng (Rotate f,p) by A3, A4, XBOOLE_0:def 3; :: 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:18;
A21: j + 1 >= 1 by NAT_1:11;
A22: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:53;
i <= len f by A7, FINSEQ_3:27;
then j <= (len f) - (p .. f) by XREAL_1:11;
then j + 1 <= len (f :- p) by A22, XREAL_1:8;
then A23: j + 1 in dom (f :- p) by A21, FINSEQ_3:27;
j + (p .. f) = i ;
then f /. i = (f :- p) /. (j + 1) by A2, A23, FINSEQ_5:55;
then x in rng (f :- p) by A9, A23, PARTFUN2:4;
hence x in rng (Rotate f,p) by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;