A1: for i being Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:36;
A2: L~ (Rotate (f,p)) = L~ f by Th33;

per cases ( N-min (L~ f) = f /. 1 or N-min (L~ f) <> f /. 1 ) ;

suppose A3: N-min (L~ f) = f /. 1 ; :: thesis: Rotate (f,p) is clockwise_oriented

then Rotate ((Rotate (f,p)),(N-min (L~ f))) = f by A1, Th16;
hence (Rotate ((Rotate (f,p)),(N-min (L~ (Rotate (f,p)))))) /. 2 in N-most (L~ (Rotate (f,p))) by A2, A3, SPRECT_2:30; :: according to SPRECT_2:def 4 :: thesis: verum

end;

suppose A4: N-min (L~ f) <> f /. 1 ; :: thesis: Rotate (f,p) is clockwise_oriented

A5: f just_once_values N-min (L~ f)

proof

take n_w_n f ; :: according to REVROT_1:def 2 :: thesis: ( n_w_n f in dom f & N-min (L~ f) = f /. (n_w_n f) & ( for z being set st z in dom f & z <> n_w_n f holds
f /. z <> N-min (L~ f) ) )
(n_w_n f) + 1 <= len f by JORDAN5D:def 15;
then A6: n_w_n f < len f by NAT_1:13;
A7: 1 <= n_w_n f by JORDAN5D:def 15;
hence A8: n_w_n f in dom f by A6, FINSEQ_3:25; :: thesis: ( N-min (L~ f) = f /. (n_w_n f) & ( for z being set st z in dom f & z <> n_w_n f holds
f /. z <> N-min (L~ f) ) )
thus A9: N-min (L~ f) = f . (n_w_n f) by JORDAN5D:def 15
.= f /. (n_w_n f) by A8, PARTFUN1:def 6 ; :: thesis: for z being set st z in dom f & z <> n_w_n f holds
f /. z <> N-min (L~ f)
let z be set ; :: thesis: ( z in dom f & z <> n_w_n f implies f /. z <> N-min (L~ f) )
assume A10: z in dom f ; :: thesis: ( not z <> n_w_n f or f /. z <> N-min (L~ f) )
then reconsider k = z as Element of NAT ;
assume A11: z <> n_w_n f ; :: thesis: f /. z <> N-min (L~ f)

per cases ( k < n_w_n f or k > n_w_n f ) by A11, XXREAL_0:1;

suppose A12: k < n_w_n f ; :: thesis: f /. z <> N-min (L~ f)

1 <= k by A10, FINSEQ_3:25;
hence f /. z <> N-min (L~ f) by A6, A9, A12, GOBOARD7:36; :: thesis: verum

end;

suppose A13: k > n_w_n f ; :: thesis: f /. z <> N-min (L~ f)

( 1 < n_w_n f & k <= len f ) by A4, A7, A9, A10, FINSEQ_3:25, XXREAL_0:1;
hence f /. z <> N-min (L~ f) by A9, A13, GOBOARD7:37; :: thesis: verum

end;

end;

end;

(Rotate (f,(N-min (L~ f)))) /. 2 in N-most (L~ f) by SPRECT_2:def 4;
hence (Rotate ((Rotate (f,p)),(N-min (L~ (Rotate (f,p)))))) /. 2 in N-most (L~ (Rotate (f,p))) by A2, A5, FINSEQ_6:105; :: according to SPRECT_2:def 4 :: thesis: verum

end;

end;