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;

suppose A3: N-min (L~ f) = f /. 1 ; :: thesis:

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:

end;

suppose A4: N-min (L~ f) <> f /. 1 ; :: thesis:

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

take n_w_n f ; :: according to FINSEQ_6:def 12 :: thesis:
(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:
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:
let z be set ; :: thesis:
assume A10: z in dom f ; :: thesis:
then reconsider k = z as Element of NAT ;
assume A11: z <> n_w_n f ; :: thesis:

per cases by A11, XXREAL_0:1;

suppose A12: k < n_w_n f ; :: thesis:

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

end;

suppose A13: k > n_w_n f ; :: thesis:

( 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:

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:

end;

end;