let D be non empty set ; for f being circular FinSequence of D
for p being Element of D st ( for i being 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; for p being Element of D st ( for i being 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; ( ( for i being 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 Nat st 1 < i & i < len f holds
f /. i <> f /. 1
; 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
;
Rotate ((Rotate (f,p)),(f /. 1)) = fA4:
f /. 1
= (f -: p) /. 1
by A2, FINSEQ_5:44;
A5:
f /. 1
= f /. (len f)
by Def1A;
then A6:
f /. 1
= (f :- p) /. (len (f :- p))
by A2, FINSEQ_5:54;
then A7:
f /. 1
in rng (f :- p)
by Th3;
A8:
f :- p just_once_values f /. 1
proof
(
p .. f <> 1 &
p .. f >= 1 )
by A2, A3, FINSEQ_4:21, FINSEQ_5:38;
then A9:
p .. f > 1
by XXREAL_0:1;
take
len (f :- p)
;
FINSEQ_6:def 12 ( 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;
( 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:54;
for z being set st z in dom (f :- p) & z <> len (f :- p) holds
(f :- p) /. z <> f /. 1
let z be
set ;
( z in dom (f :- p) & z <> len (f :- p) implies (f :- p) /. z <> f /. 1 )
assume A10:
z in dom (f :- p)
;
( not z <> len (f :- p) or (f :- p) /. z <> f /. 1 )
then reconsider k =
z as
Element of
NAT ;
k <> 0
by A10, FINSEQ_3:25;
then consider i being
Nat such that A11:
k = i + 1
by NAT_1:6;
assume A12:
z <> len (f :- p)
;
(f :- p) /. z <> f /. 1
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
k <= len (f :- p)
by A10, FINSEQ_3:25;
then
k < len (f :- p)
by A12, XXREAL_0:1;
then
i + 1
< ((len f) - (p .. f)) + 1
by A2, A11, FINSEQ_5:50;
then
i < (len f) - (p .. f)
by XREAL_1:6;
then A13:
i + (p .. f) < len f
by XREAL_1:20;
p .. f <= i + (p .. f)
by NAT_1:11;
then A14:
1
< i + (p .. f)
by A9, XXREAL_0:2;
(f :- p) /. (i + 1) = f /. (i + (p .. f))
by A2, A10, A11, FINSEQ_5:52;
hence
(f :- p) /. z <> f /. 1
by A1, A11, A14, A13;
verum
end;
f /. 1
in rng f
by A2, Th42, RELAT_1:38;
then A15:
f /. 1
in rng (Rotate (f,p))
by A2, Th90;
Rotate (
f,
p)
= (f :- p) ^ ((f -: p) /^ 1)
by A2, Def2;
hence Rotate (
(Rotate (f,p)),
(f /. 1)) =
(((f :- p) ^ ((f -: p) /^ 1)) :- (f /. 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1)
by A15, Def2
.=
(((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ ((((f :- p) ^ ((f -: p) /^ 1)) -: (f /. 1)) /^ 1)
by A7, Th64
.=
(((f :- p) :- (f /. 1)) ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1)
by A7, Th66
.=
(<*(f /. 1)*> ^ ((f -: p) /^ 1)) ^ (((f :- p) -: (f /. 1)) /^ 1)
by A6, A8, Th5
.=
(f -: p) ^ (((f :- p) -: (f /. 1)) /^ 1)
by A2, A4, FINSEQ_5:29, FINSEQ_5:47
.=
(f -: p) ^ ((f :- p) /^ 1)
by A6, A8, Th4
.=
f
by A2, Th76
;
verum end;