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) )
per cases ( p1 in rng f or not p1 in rng f ) ;
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 ;
now :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
per cases ( rng f is trivial or not rng f is trivial ) ;
suppose rng f is trivial ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
then p1 = p2 by ;
hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th93; :: thesis: verum
end;
suppose A5: not rng f is trivial ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
then f = <*(f /. 1)*> ^ (f /^ 1) by ;
then A6: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;
hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by ; :: thesis: verum
end;
end;
end;
hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ; :: thesis: verum
end;
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;
end;