let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
p in rng (Rotate f,p)
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
p in rng (Rotate f,p)
let f be FinSequence of D; :: thesis: ( p in rng f implies p in rng (Rotate f,p) )
assume p in rng f ; :: thesis: p in rng (Rotate f,p)
then Rotate f,p = (f :- p) ^ ((f -: p) /^ 1) by Def2;
then A1: rng (Rotate f,p) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:44;
p in {p} by TARSKI:def 1;
then p in rng <*p*> by FINSEQ_1:56;
then p in (rng <*p*>) \/ (rng (f /^ (p .. f))) by XBOOLE_0:def 3;
then p in rng (<*p*> ^ (f /^ (p .. f))) by FINSEQ_1:44;
then p in rng (f :- p) by FINSEQ_5:def 2;
hence p in rng (Rotate f,p) by A1, XBOOLE_0:def 3; :: thesis: verum