per cases ( not p in rng f or p in rng f ) ;

suppose not p in rng f ; :: thesis: not Rotate f,p is constant

hence not Rotate f,p is constant by FINSEQ_6:def 2; :: thesis: verum

end;

suppose A1: p in rng f ; :: thesis: not Rotate f,p is constant

consider n, m being Element of NAT such that
A2: n in dom f and
A3: m in dom f and
A4: f /. n <> f /. m by Def1;
A5: dom (Rotate f,p) = dom f by Th15;
A6: ( 1 <= n & n <= len f ) by A2, FINSEQ_3:27;
A7: ( 1 <= m & m <= len f ) by A3, FINSEQ_3:27;
thus not Rotate f,p is constant :: thesis: verum

proof

A8: p .. f <= len f by A1, FINSEQ_4:31;
A9: 1 <= p .. f by A1, FINSEQ_4:31;

per cases ( ( n <= p .. f & m <= p .. f ) or ( n <= p .. f & m >= p .. f ) or ( m <= p .. f & n >= p .. f ) or ( m >= p .. f & n >= p .. f ) ) ;

suppose that A10: n <= p .. f and
A11: m <= p .. f ; :: thesis: not Rotate f,p is constant

A12: f /. n = (Rotate f,p) /. ((n + (len f)) -' (p .. f)) by A1, A6, A10, Th18;
A13: f /. m = (Rotate f,p) /. ((m + (len f)) -' (p .. f)) by A1, A7, A11, Th18;
n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by A6, XXREAL_0:2;
then A14: 1 <= (n + (len f)) -' (p .. f) by A8, NAT_D:38;
n + (len f) <= (len f) + (p .. f) by A10, XREAL_1:8;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A15: (n + (len f)) -' (p .. f) in dom f by A14, FINSEQ_3:27;
m <= m + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= m + ((len f) -' (p .. f)) by A7, XXREAL_0:2;
then A16: 1 <= (m + (len f)) -' (p .. f) by A8, NAT_D:38;
m + (len f) <= (len f) + (p .. f) by A11, XREAL_1:8;
then (m + (len f)) -' (p .. f) <= len f by NAT_D:53;
then (m + (len f)) -' (p .. f) in dom f by A16, FINSEQ_3:27;
hence not Rotate f,p is constant by A4, A5, A12, A13, A15, Def1; :: thesis: verum

end;

suppose that A17: n <= p .. f and
A18: m >= p .. f ; :: thesis: not Rotate f,p is constant

A19: f /. n = (Rotate f,p) /. ((n + (len f)) -' (p .. f)) by A1, A6, A17, Th18;
A20: f /. m = (Rotate f,p) /. ((m + 1) -' (p .. f)) by A1, A7, A18, Th10;
n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by A6, XXREAL_0:2;
then A21: 1 <= (n + (len f)) -' (p .. f) by A8, NAT_D:38;
n + (len f) <= (len f) + (p .. f) by A17, XREAL_1:8;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A22: (n + (len f)) -' (p .. f) in dom f by A21, FINSEQ_3:27;
1 + (p .. f) <= m + 1 by A18, XREAL_1:8;
then A23: 1 <= (m + 1) -' (p .. f) by NAT_D:55;
m + 1 <= (len f) + (p .. f) by A7, A9, XREAL_1:9;
then (m + 1) -' (p .. f) <= len f by NAT_D:53;
then (m + 1) -' (p .. f) in dom f by A23, FINSEQ_3:27;
hence not Rotate f,p is constant by A4, A5, A19, A20, A22, Def1; :: thesis: verum

end;

suppose that A24: m <= p .. f and
A25: n >= p .. f ; :: thesis: not Rotate f,p is constant

A26: f /. m = (Rotate f,p) /. ((m + (len f)) -' (p .. f)) by A1, A7, A24, Th18;
A27: f /. n = (Rotate f,p) /. ((n + 1) -' (p .. f)) by A1, A6, A25, Th10;
m <= m + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= m + ((len f) -' (p .. f)) by A7, XXREAL_0:2;
then A28: 1 <= (m + (len f)) -' (p .. f) by A8, NAT_D:38;
m + (len f) <= (len f) + (p .. f) by A24, XREAL_1:8;
then (m + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A29: (m + (len f)) -' (p .. f) in dom f by A28, FINSEQ_3:27;
1 + (p .. f) <= n + 1 by A25, XREAL_1:8;
then A30: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
n + 1 <= (len f) + (p .. f) by A6, A9, XREAL_1:9;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then (n + 1) -' (p .. f) in dom f by A30, FINSEQ_3:27;
hence not Rotate f,p is constant by A4, A5, A26, A27, A29, Def1; :: thesis: verum

end;

suppose that A31: m >= p .. f and
A32: n >= p .. f ; :: thesis: not Rotate f,p is constant

A33: f /. m = (Rotate f,p) /. ((m + 1) -' (p .. f)) by A1, A7, A31, Th10;
A34: f /. n = (Rotate f,p) /. ((n + 1) -' (p .. f)) by A1, A6, A32, Th10;
1 + (p .. f) <= m + 1 by A31, XREAL_1:8;
then A35: 1 <= (m + 1) -' (p .. f) by NAT_D:55;
m + 1 <= (len f) + (p .. f) by A7, A9, XREAL_1:9;
then (m + 1) -' (p .. f) <= len f by NAT_D:53;
then A36: (m + 1) -' (p .. f) in dom f by A35, FINSEQ_3:27;
1 + (p .. f) <= n + 1 by A32, XREAL_1:8;
then A37: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
n + 1 <= (len f) + (p .. f) by A6, A9, XREAL_1:9;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then (n + 1) -' (p .. f) in dom f by A37, FINSEQ_3:27;
hence not Rotate f,p is constant by A4, A5, A33, A34, A36, Def1; :: thesis: verum

end;

end;

end;

end;

end;