let D be non empty set ; for p being Element of D
for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)
let p be Element of D; for f being FinSequence of D holds Rotate ((Rotate (f,p)),p) = Rotate (f,p)
let f be FinSequence of D; Rotate ((Rotate (f,p)),p) = Rotate (f,p)
per cases
( p in rng f or not p in rng f )
;
suppose A1:
p in rng f
;
Rotate ((Rotate (f,p)),p) = Rotate (f,p)then reconsider f9 =
f as non
empty FinSequence of
D ;
A2:
(Rotate (f,p)) /. 1
= p
by A1, Th92;
then A3:
(Rotate (f9,p)) :- p = Rotate (
f,
p)
by Th44;
A4:
p in rng (Rotate (f,p))
by A1, Th91;
A5:
len <*p*> = 1
by FINSEQ_1:39;
(Rotate (f9,p)) -: p = <*p*>
by A2, Th44;
hence Rotate (
(Rotate (f,p)),
p) =
(Rotate (f,p)) ^ (<*p*> /^ 1)
by A3, A4, Def2
.=
(Rotate (f,p)) ^ {}
by A5, FINSEQ_5:32
.=
Rotate (
f,
p)
by FINSEQ_1:34
;
verum end; end;