let i be Element of NAT ; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f))
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f))
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f))
let f be FinSequence of D; :: thesis: ( p in rng f & len (f :- p) < i & i <= len f implies (Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f)) )
assume that
A1: p in rng f and
A2: len (f :- p) < i and
A3: i <= len f ; :: thesis: (Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f))
A4: len (f -: p) = p .. f by A1, FINSEQ_5:45;
A5: ( (i -' (len (f :- p))) + (len (f :- p)) = i & Rotate f,p = (f :- p) ^ ((f -: p) /^ 1) ) by A1, A2, FINSEQ_6:def 2, XREAL_1:237;
not f -: p is empty by A1, FINSEQ_5:50;
then len (f -: p) >= 1 by NAT_1:14;
then A6: len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 2;
i + (p .. f) <= (p .. f) + (len f) by A3, XREAL_1:8;
then A7: (i + (p .. f)) -' (len f) <= p .. f by NAT_D:53;
A8: p .. f <= len f by A1, FINSEQ_4:31;
then (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:235;
then A9: len (f :- p) = ((len f) -' (p .. f)) + 1 by A1, FINSEQ_5:53;
then A10: (len f) -' (p .. f) < i by A2, NAT_1:13;
then A11: len f < i + (p .. f) by NAT_D:55;
then (len f) + 1 <= i + (p .. f) by NAT_1:13;
then 1 <= (i + (p .. f)) -' (len f) by NAT_D:55;
then A12: (i + (p .. f)) -' (len f) in Seg (p .. f) by A7, FINSEQ_1:3;
i <= (p .. f) + ((len f) -' (p .. f)) by A3, A8, XREAL_1:237;
then i -' ((len f) -' (p .. f)) <= p .. f by NAT_D:53;
then (i -' (((len f) -' (p .. f)) + 1)) + 1 <= p .. f by A10, NAT_2:9;
then A13: i -' (len (f :- p)) <= (len (f -: p)) - 1 by A9, A4, XREAL_1:21;
(((len f) -' (p .. f)) + 1) + 1 <= i by A2, A9, NAT_1:13;
then A14: 1 <= i -' (((len f) -' (p .. f)) + 1) by NAT_D:55;
then A15: i -' (((len f) -' (p .. f)) + 1) in dom ((f -: p) /^ 1) by A9, A6, A13, FINSEQ_3:27;
(len f) - (p .. f) = (len f) -' (p .. f) by A8, XREAL_1:235;
then 1 <= i -' (len (f :- p)) by A1, A14, FINSEQ_5:53;
then i -' (len (f :- p)) in dom ((f -: p) /^ 1) by A6, A13, FINSEQ_3:27;
hence (Rotate f,p) /. i = ((f -: p) /^ 1) /. (i -' (((len f) -' (p .. f)) + 1)) by A9, A5, FINSEQ_4:84
.= (f -: p) /. ((i -' (((len f) -' (p .. f)) + 1)) + 1) by A15, FINSEQ_5:30
.= (f -: p) /. (i -' ((len f) -' (p .. f))) by A10, NAT_2:9
.= (f -: p) /. (i - ((len f) -' (p .. f))) by A10, XREAL_1:235
.= (f -: p) /. (i - ((len f) - (p .. f))) by A8, XREAL_1:235
.= (f -: p) /. ((i + (p .. f)) - (len f))
.= (f -: p) /. ((i + (p .. f)) -' (len f)) by A11, XREAL_1:235
.= f /. ((i + (p .. f)) -' (len f)) by A1, A12, FINSEQ_5:46 ;
:: thesis: verum