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 Def2; :: thesis: verum

end;

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

A2: dom (Rotate (f,p)) = dom f by Th15;
consider n, m being Nat such that
A3: n in dom f and
A4: m in dom f and
A5: f /. n <> f /. m by Def1;
A6: n <= len f by A3, FINSEQ_3:25;
A7: m <= len f by A4, FINSEQ_3:25;
A8: 1 <= m by A4, FINSEQ_3:25;
A9: 1 <= n by A3, FINSEQ_3:25;
thus Rotate (f,p) is constant :: thesis: verum

proof

A10: 1 <= p .. f by A1, FINSEQ_4:21;
A11: p .. f <= len f by A1, FINSEQ_4:21;

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 A12: n <= p .. f and
A13: m <= p .. f ; :: thesis: Rotate (f,p) is constant

n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by A9, XXREAL_0:2;
then A14: 1 <= (n + (len f)) -' (p .. f) by A11, NAT_D:38;
m <= m + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= m + ((len f) -' (p .. f)) by A8, XXREAL_0:2;
then A15: 1 <= (m + (len f)) -' (p .. f) by A11, NAT_D:38;
m + (len f) <= (len f) + (p .. f) by A13, XREAL_1:6;
then (m + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A16: (m + (len f)) -' (p .. f) in dom f by A15, FINSEQ_3:25;
n + (len f) <= (len f) + (p .. f) by A12, XREAL_1:6;
then (n + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A17: (n + (len f)) -' (p .. f) in dom f by A14, FINSEQ_3:25;
( f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) & f /. m = (Rotate (f,p)) /. ((m + (len f)) -' (p .. f)) ) by A1, A9, A8, A12, A13, Th18;
hence Rotate (f,p) is constant by A5, A2, A17, A16; :: thesis: verum

end;

suppose that A18: n <= p .. f and
A19: m >= p .. f ; :: thesis: Rotate (f,p) is constant

1 + (p .. f) <= m + 1 by A19, XREAL_1:6;
then A20: 1 <= (m + 1) -' (p .. f) by NAT_D:55;
n <= n + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= n + ((len f) -' (p .. f)) by A9, XXREAL_0:2;
then A21: 1 <= (n + (len f)) -' (p .. f) by A11, NAT_D:38;
n + (len f) <= (len f) + (p .. f) by A18, XREAL_1:6;
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:25;
m + 1 <= (len f) + (p .. f) by A7, A10, XREAL_1:7;
then (m + 1) -' (p .. f) <= len f by NAT_D:53;
then A23: (m + 1) -' (p .. f) in dom f by A20, FINSEQ_3:25;
( f /. n = (Rotate (f,p)) /. ((n + (len f)) -' (p .. f)) & f /. m = (Rotate (f,p)) /. ((m + 1) -' (p .. f)) ) by A1, A9, A7, A18, A19, Th10, Th18;
hence Rotate (f,p) is constant by A5, A2, A22, A23; :: thesis: verum

end;

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

1 + (p .. f) <= n + 1 by A25, XREAL_1:6;
then A26: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
m <= m + ((len f) -' (p .. f)) by NAT_1:11;
then 1 <= m + ((len f) -' (p .. f)) by A8, XXREAL_0:2;
then A27: 1 <= (m + (len f)) -' (p .. f) by A11, NAT_D:38;
m + (len f) <= (len f) + (p .. f) by A24, XREAL_1:6;
then (m + (len f)) -' (p .. f) <= len f by NAT_D:53;
then A28: (m + (len f)) -' (p .. f) in dom f by A27, FINSEQ_3:25;
n + 1 <= (len f) + (p .. f) by A6, A10, XREAL_1:7;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then A29: (n + 1) -' (p .. f) in dom f by A26, FINSEQ_3:25;
( f /. m = (Rotate (f,p)) /. ((m + (len f)) -' (p .. f)) & f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) ) by A1, A6, A8, A24, A25, Th10, Th18;
hence Rotate (f,p) is constant by A5, A2, A28, A29; :: thesis: verum

end;

suppose that A30: m >= p .. f and
A31: n >= p .. f ; :: thesis: Rotate (f,p) is constant

1 + (p .. f) <= m + 1 by A30, XREAL_1:6;
then A32: 1 <= (m + 1) -' (p .. f) by NAT_D:55;
1 + (p .. f) <= n + 1 by A31, XREAL_1:6;
then A33: 1 <= (n + 1) -' (p .. f) by NAT_D:55;
n + 1 <= (len f) + (p .. f) by A6, A10, XREAL_1:7;
then (n + 1) -' (p .. f) <= len f by NAT_D:53;
then A34: (n + 1) -' (p .. f) in dom f by A33, FINSEQ_3:25;
m + 1 <= (len f) + (p .. f) by A7, A10, XREAL_1:7;
then (m + 1) -' (p .. f) <= len f by NAT_D:53;
then A35: (m + 1) -' (p .. f) in dom f by A32, FINSEQ_3:25;
( f /. m = (Rotate (f,p)) /. ((m + 1) -' (p .. f)) & f /. n = (Rotate (f,p)) /. ((n + 1) -' (p .. f)) ) by A1, A6, A7, A30, A31, Th10;
hence Rotate (f,p) is constant by A5, A2, A35, A34; :: thesis: verum

end;

end;

end;

end;

end;