let D be non empty set ; :: thesis: for p1, p2 being Element of D

for f being FinSequence of D st f is circular & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let p1, p2 be Element of D; :: thesis: for f being FinSequence of D st f is circular & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

for f being FinSequence of D st f is circular & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let p1, p2 be Element of D; :: thesis: for f being FinSequence of D st f is circular & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

per cases
( p1 in rng f or not p1 in rng f )
;

end;

suppose A1:
p1 in rng f
; :: thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

assume that

A2: f is circular and

A3: f just_once_values p2 ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

A4: p2 in rng f by A3, FINSEQ_4:45;

end;A2: f is circular and

A3: f just_once_values p2 ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

A4: p2 in rng f by A3, FINSEQ_4:45;

now :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)end;

hence
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
; :: thesis: verumper cases
( rng f is trivial or not rng f is trivial )
;

end;

suppose
rng f is trivial
; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

then
p1 = p2
by A1, A4, ZFMISC_1:def 10;

hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th93; :: thesis: verum

end;hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th93; :: thesis: verum

suppose A5:
not rng f is trivial
; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

then
f = <*(f /. 1)*> ^ (f /^ 1)
by FINSEQ_5:29, RELAT_1:38;

then A6: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;

end;then A6: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;

now :: thesis: p2 in rng (f /^ 1)

hence
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
by A3, Th104; :: thesis: verum
not f is trivial
by A5;

then len f >= 1 + 1 by NAT_D:60;

then A7: 1 < len f by NAT_1:13;

assume A8: not p2 in rng (f /^ 1) ; :: thesis: contradiction

then p2 in rng <*(f /. 1)*> by A4, A6, XBOOLE_0:def 3;

then p2 in {(f /. 1)} by FINSEQ_1:39;

then p2 = f /. 1 by TARSKI:def 1;

then A9: p2 = f /. (len f) by A2;

len f in dom f by A5, FINSEQ_5:6, RELAT_1:38;

hence contradiction by A8, A9, A7, Th58; :: thesis: verum

end;then len f >= 1 + 1 by NAT_D:60;

then A7: 1 < len f by NAT_1:13;

assume A8: not p2 in rng (f /^ 1) ; :: thesis: contradiction

then p2 in rng <*(f /. 1)*> by A4, A6, XBOOLE_0:def 3;

then p2 in {(f /. 1)} by FINSEQ_1:39;

then p2 = f /. 1 by TARSKI:def 1;

then A9: p2 = f /. (len f) by A2;

len f in dom f by A5, FINSEQ_5:6, RELAT_1:38;

hence contradiction by A8, A9, A7, Th58; :: thesis: verum

suppose
not p1 in rng f
; :: thesis: ( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

hence
( f is circular & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )
by Def2; :: thesis: verum

end;