let D be non empty set ; :: thesis: for f being circular FinSequence of D
for p being Element of D st ( for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate (Rotate f,p),(f /. 1) = f
let f be circular FinSequence of D; :: thesis: for p being Element of D st ( for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 ) holds
Rotate (Rotate f,p),(f /. 1) = f
let p be Element of D; :: thesis: ( ( for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 ) implies Rotate (Rotate f,p),(f /. 1) = f )
assume A1:
for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1
; :: thesis: Rotate (Rotate f,p),(f /. 1) = f
per cases
( not p in rng f or p = f /. 1 or ( p in rng f & p <> f /. 1 ) )
;
suppose that A2:
p in rng f
and A3:
p <> f /. 1
;
:: thesis: Rotate (Rotate f,p),(f /. 1) = fA4:
Rotate f,
p = (f :- p) ^ ((f -: p) /^ 1)
by A2, FINSEQ_6:def 2;
A5:
f /. 1
= f /. (len f)
by FINSEQ_6:def 1;
then A6:
f /. 1
= (f :- p) /. (len (f :- p))
by A2, FINSEQ_5:57;
then A7:
f /. 1
in rng (f :- p)
by Th3;
A8:
f :- p just_once_values f /. 1
proof
take
len (f :- p)
;
:: according to REVROT_1:def 2 :: thesis: ( len (f :- p) in dom (f :- p) & f /. 1 = (f :- p) /. (len (f :- p)) & ( for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1 ) )
thus
len (f :- p) in dom (f :- p)
by FINSEQ_5:6;
:: thesis: ( f /. 1 = (f :- p) /. (len (f :- p)) & ( for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1 ) )
thus
f /. 1
= (f :- p) /. (len (f :- p))
by A2, A5, FINSEQ_5:57;
:: thesis: for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1
let z be
set ;
:: thesis: ( z in dom (f :- p) & z <> len (f :- p) implies (f :- p) /. z <> f /. 1 )
assume A9:
z in dom (f :- p)
;
:: thesis: ( not z <> len (f :- p) or (f :- p) /. z <> f /. 1 )
then reconsider k =
z as
Element of
NAT ;
k <> 0
by A9, FINSEQ_3:27;
then consider i being
Nat such that A10:
k = i + 1
by NAT_1:6;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
A11:
(f :- p) /. (i + 1) = f /. (i + (p .. f))
by A2, A9, A10, FINSEQ_5:55;
A12:
p .. f <> 1
by A2, A3, FINSEQ_5:41;
p .. f >= 1
by A2, FINSEQ_4:31;
then A13:
p .. f > 1
by A12, XXREAL_0:1;
p .. f <= i + (p .. f)
by NAT_1:11;
then A14:
1
< i + (p .. f)
by A13, XXREAL_0:2;
assume A15:
z <> len (f :- p)
;
:: thesis: (f :- p) /. z <> f /. 1
k <= len (f :- p)
by A9, FINSEQ_3:27;
then
k < len (f :- p)
by A15, XXREAL_0:1;
then
i + 1
< ((len f) - (p .. f)) + 1
by A2, A10, FINSEQ_5:53;
then
i < (len f) - (p .. f)
by XREAL_1:8;
then
i + (p .. f) < len f
by XREAL_1:22;
hence
(f :- p) /. z <> f /. 1
by A1, A10, A11, A14;
:: thesis: verum
end; A16:
f /. 1
= (f -: p) /. 1
by A2, FINSEQ_5:47;
f /. 1
in rng f
by A2, FINSEQ_6:46, RELAT_1:60;
then
f /. 1
in rng (Rotate f,p)
by A2, FINSEQ_6:96;
hence Rotate (Rotate f,p),
(f /. 1) =
(((f :- p) ^ ((f -: p) /^ 1)) :- (f /. 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1)
by A4, FINSEQ_6:def 2
.=
(((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1)
by A7, FINSEQ_6:69
.=
(((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1)
by A7, FINSEQ_6:71
.=
(<*(f /. 1)*> ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1)
by A6, A8, Th5
.=
(f -: p) ^ (((f :- p) -: (f /. 1)) /^ 1)
by A2, A16, FINSEQ_5:32, FINSEQ_5:50
.=
(f -: p) ^ ((f :- p) /^ 1)
by A6, A8, Th4
.=
f
by A2, FINSEQ_6:81
;
:: thesis: verum end;