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)) )
p in {p} by TARSKI:def 1;
then p in rng <*p*> by FINSEQ_1:39;
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:31;
then A1: p in rng (f :- p) by FINSEQ_5:def 2;
assume p in rng f ; :: thesis: p in rng (Rotate (f,p))
then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2;
then rng (Rotate (f,p)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31;
hence p in rng (Rotate (f,p)) by A1, XBOOLE_0:def 3; :: thesis: verum