let D be non empty set ; :: thesis: for p1, p2 being Element of D
for f being FinSequence of D st p2 in rng (f /^ 1) & 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 p2 in rng (f /^ 1) & f just_once_values p2 holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( p2 in rng (f /^ 1) & 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: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )
assume that
A2: p2 in rng (f /^ 1) and
A3: f just_once_values p2 ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by ;
then A4: p2 in (rng ((f -| p1) ^ <*p1*>)) \+\ (rng (f |-- p1)) by ;
A5: now :: thesis: ( ( p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f |-- p1) & ( p2 in rng (f :- p1) implies p1 = p2 ) ) or ( not p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f -: p1) ) )
per cases ( ( p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f |-- p1) ) or not p2 in rng ((f -| p1) ^ <*p1*>) ) by ;
case that p2 in rng ((f -| p1) ^ <*p1*>) and
A6: not p2 in rng (f |-- p1) ; :: thesis: ( p2 in rng (f :- p1) implies p1 = p2 )
now :: thesis: ( ( not p2 in rng <*p1*> & not p2 in rng (f :- p1) ) or ( p2 in rng <*p1*> & p2 = p1 ) )end;
hence ( p2 in rng (f :- p1) implies p1 = p2 ) ; :: thesis: verum
end;
case not p2 in rng ((f -| p1) ^ <*p1*>) ; :: thesis: not p2 in rng (f -: p1)
hence not p2 in rng (f -: p1) by ; :: thesis: verum
end;
end;
end;
A7: p2 in rng f by ;
then f = <*(f /. 1)*> ^ (f /^ 1) by ;
then p2 in (rng <*(f /. 1)*>) \+\ (rng (f /^ 1)) by ;
then not p2 in rng <*(f /. 1)*> by ;
then not p2 in {(f /. 1)} by FINSEQ_1:39;
then p2 <> f /. 1 by TARSKI:def 1;
then A8: p2 .. f <> 1 by ;
now :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
per cases ( p1 = p2 or p2 in (rng f) \ (rng (f -: p1)) or p2 in (rng f) \ (rng (f :- p1)) ) by ;
suppose p1 = p2 ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th93; :: thesis: verum
end;
suppose p2 in (rng f) \ (rng (f -: p1)) ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Th102; :: thesis: verum
end;
suppose p2 in (rng f) \ (rng (f :- p1)) ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
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: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )
hence ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) ) by Def2; :: thesis: verum
end;
end;