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 & 1 <= i & i <= len (f :- p) holds
(Rotate f,p) /. i = f /. ((i -' 1) + (p .. 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 & 1 <= i & i <= len (f :- p) holds
(Rotate f,p) /. i = f /. ((i -' 1) + (p .. f))
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds
(Rotate f,p) /. i = f /. ((i -' 1) + (p .. f))
let f be FinSequence of D; :: thesis: ( p in rng f & 1 <= i & i <= len (f :- p) implies (Rotate f,p) /. i = f /. ((i -' 1) + (p .. f)) )
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i <= len (f :- p) ; :: thesis: (Rotate f,p) /. i = f /. ((i -' 1) + (p .. f))
A4: i = (i -' 1) + 1 by A2, XREAL_1:237;
A5: i in dom (f :- p) by A2, A3, FINSEQ_3:27;
Rotate f,p = (f :- p) ^ ((f -: p) /^ 1) by A1, FINSEQ_6:def 2;
hence (Rotate f,p) /. i = (f :- p) /. i by A5, FINSEQ_4:83
.= f /. ((i -' 1) + (p .. f)) by A1, A4, A5, FINSEQ_5:55 ;
:: thesis: verum