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

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 V25() :: thesis: verum

end;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 V25() :: thesis: verum

proof

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

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

end;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 ) )
;

end;

suppose that A12:
n <= p .. f
and

A13: m <= p .. f ; :: thesis: Rotate (f,p) is V25()

A13: m <= p .. f ; :: thesis: Rotate (f,p) is V25()

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 V25() by A5, A2, A17, A16; :: thesis: verum

end;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 V25() by A5, A2, A17, A16; :: thesis: verum

suppose that A18:
n <= p .. f
and

A19: m >= p .. f ; :: thesis: Rotate (f,p) is V25()

A19: m >= p .. f ; :: thesis: Rotate (f,p) is V25()

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 V25() by A5, A2, A22, A23; :: thesis: verum

end;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 V25() by A5, A2, A22, A23; :: thesis: verum

suppose that A24:
m <= p .. f
and

A25: n >= p .. f ; :: thesis: Rotate (f,p) is V25()

A25: n >= p .. f ; :: thesis: Rotate (f,p) is V25()

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 V25() by A5, A2, A28, A29; :: thesis: verum

end;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 V25() by A5, A2, A28, A29; :: thesis: verum

suppose that A30:
m >= p .. f
and

A31: n >= p .. f ; :: thesis: Rotate (f,p) is V25()

A31: n >= p .. f ; :: thesis: Rotate (f,p) is V25()

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 V25() by A5, A2, A35, A34; :: thesis: verum

end;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 V25() by A5, A2, A35, A34; :: thesis: verum