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

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