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

(Rotate (f,p)) /. 1 = p

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. 1 = p

let f be FinSequence of D; :: thesis: ( p in rng f implies (Rotate (f,p)) /. 1 = p )

assume p in rng f ; :: thesis: (Rotate (f,p)) /. 1 = p

then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2

.= (<*p*> ^ (f /^ (p .. f))) ^ ((f -: p) /^ 1) by FINSEQ_5:def 2

.= <*p*> ^ ((f /^ (p .. f)) ^ ((f -: p) /^ 1)) by FINSEQ_1:32 ;

hence (Rotate (f,p)) /. 1 = p by FINSEQ_5:15; :: thesis: verum

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. 1 = p

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. 1 = p

let f be FinSequence of D; :: thesis: ( p in rng f implies (Rotate (f,p)) /. 1 = p )

assume p in rng f ; :: thesis: (Rotate (f,p)) /. 1 = p

then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2

.= (<*p*> ^ (f /^ (p .. f))) ^ ((f -: p) /^ 1) by FINSEQ_5:def 2

.= <*p*> ^ ((f /^ (p .. f)) ^ ((f -: p) /^ 1)) by FINSEQ_1:32 ;

hence (Rotate (f,p)) /. 1 = p by FINSEQ_5:15; :: thesis: verum