A1: for i being 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 FINSEQ_6:def 12 :: thesis: ( n_w_n f in dom f & N-min (L~ f) = f /. (n_w_n f) & ( for b₁ being set holds
( not b₁ in dom f or b₁ = n_w_n f or not f /. b₁ = 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 b₁ being set holds
( not b₁ in dom f or b₁ = n_w_n f or not f /. b₁ = 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 b₁ being set holds
( not b₁ in dom f or b₁ = n_w_n f or not f /. b₁ = N-min (L~ f) )
let z be set ; :: thesis: ( not z in dom f or z = n_w_n f or not f /. z = N-min (L~ f) )
assume A10: z in dom f ; :: thesis: ( z = n_w_n f or not f /. z = N-min (L~ f) )
then reconsider k = z as Element of NAT ;
assume A11: z <> n_w_n f ; :: thesis: not 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: not f /. z = N-min (L~ f)

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

end;

suppose A13: k > n_w_n f ; :: thesis: not 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 not 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;