let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st f is circular & p in rng f holds

rng (Rotate (f,p)) = rng f

let p be Element of D; :: thesis: for f being FinSequence of D st f is circular & p in rng f holds

rng (Rotate (f,p)) = rng f

let f be FinSequence of D; :: thesis: ( f is circular & p in rng f implies rng (Rotate (f,p)) = rng f )

assume that

A1: f is circular and

A2: p in rng f ; :: thesis: rng (Rotate (f,p)) = rng f

A3: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A2, Def2;

A4: rng ((f -: p) /^ 1) c= rng (f -: p) by FINSEQ_5:33;

rng (f -: p) c= rng f by FINSEQ_5:48;

then A5: rng ((f -: p) /^ 1) c= rng f by A4;

A6: rng ((f :- p) ^ ((f -: p) /^ 1)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31;

rng (f :- p) c= rng f by A2, FINSEQ_5:55;

hence rng (Rotate (f,p)) c= rng f by A3, A6, A5, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (Rotate (f,p))

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in rng (Rotate (f,p)) )

assume x in rng f ; :: thesis: x in rng (Rotate (f,p))

then consider i being Nat such that

A7: i in dom f and

A8: f . i = x by FINSEQ_2:10;

A9: x = f /. i by A7, A8, PARTFUN1:def 6;

for f being FinSequence of D st f is circular & p in rng f holds

rng (Rotate (f,p)) = rng f

let p be Element of D; :: thesis: for f being FinSequence of D st f is circular & p in rng f holds

rng (Rotate (f,p)) = rng f

let f be FinSequence of D; :: thesis: ( f is circular & p in rng f implies rng (Rotate (f,p)) = rng f )

assume that

A1: f is circular and

A2: p in rng f ; :: thesis: rng (Rotate (f,p)) = rng f

A3: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A2, Def2;

A4: rng ((f -: p) /^ 1) c= rng (f -: p) by FINSEQ_5:33;

rng (f -: p) c= rng f by FINSEQ_5:48;

then A5: rng ((f -: p) /^ 1) c= rng f by A4;

A6: rng ((f :- p) ^ ((f -: p) /^ 1)) = (rng (f :- p)) \/ (rng ((f -: p) /^ 1)) by FINSEQ_1:31;

rng (f :- p) c= rng f by A2, FINSEQ_5:55;

hence rng (Rotate (f,p)) c= rng f by A3, A6, A5, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (Rotate (f,p))

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in rng (Rotate (f,p)) )

assume x in rng f ; :: thesis: x in rng (Rotate (f,p))

then consider i being Nat such that

A7: i in dom f and

A8: f . i = x by FINSEQ_2:10;

A9: x = f /. i by A7, A8, PARTFUN1:def 6;

per cases
( i = 1 or ( i <= p .. f & i <> 1 ) or i > p .. f )
;

end;

suppose A10:
i = 1
; :: thesis: x in rng (Rotate (f,p))

len (f :- p) =
len (<*p*> ^ (f /^ (p .. f)))
by FINSEQ_5:def 2

.= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:22

.= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ;

then 1 <= len (f :- p) by NAT_1:11;

then A11: len (f :- p) in dom (f :- p) by FINSEQ_3:25;

x = (f :- p) /. (len (f :- p)) by A2, FINSEQ_5:54, A1, A9, A10;

then x in rng (f :- p) by A11, PARTFUN2:2;

hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def 3; :: thesis: verum

end;.= (len <*p*>) + (len (f /^ (p .. f))) by FINSEQ_1:22

.= 1 + (len (f /^ (p .. f))) by FINSEQ_1:39 ;

then 1 <= len (f :- p) by NAT_1:11;

then A11: len (f :- p) in dom (f :- p) by FINSEQ_3:25;

x = (f :- p) /. (len (f :- p)) by A2, FINSEQ_5:54, A1, A9, A10;

then x in rng (f :- p) by A11, PARTFUN2:2;

hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def 3; :: thesis: verum

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

A13: i <> 1 ; :: thesis: x in rng (Rotate (f,p))

A13: i <> 1 ; :: thesis: x in rng (Rotate (f,p))

A14:
i <> 0
by A7, FINSEQ_3:25;

then A15: i > 0 + 1 by A13, NAT_1:25;

then A16: i in Seg (p .. f) by A12;

consider j being Nat such that

A17: i = j + 1 by A14, NAT_1:6;

A18: j >= 1 by A15, A17, NAT_1:14;

A19: i <= len (f -: p) by A2, A12, FINSEQ_5:42;

then 1 <= len (f -: p) by A14, NAT_1:25, XXREAL_0:2;

then len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 1;

then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ;

then j <= len ((f -: p) /^ 1) by A17, A19, XREAL_1:6;

then A20: j in dom ((f -: p) /^ 1) by A18, FINSEQ_3:25;

A21: len <*((f -: p) /. 1)*> = 1 by FINSEQ_1:39;

f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by A2, FINSEQ_5:29, FINSEQ_5:47;

then ((f -: p) /^ 1) /. j = (f -: p) /. i by A17, A20, A21, FINSEQ_4:69

.= f /. i by A2, A16, FINSEQ_5:43 ;

then x in rng ((f -: p) /^ 1) by A9, A20, PARTFUN2:2;

hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def 3; :: thesis: verum

end;then A15: i > 0 + 1 by A13, NAT_1:25;

then A16: i in Seg (p .. f) by A12;

consider j being Nat such that

A17: i = j + 1 by A14, NAT_1:6;

A18: j >= 1 by A15, A17, NAT_1:14;

A19: i <= len (f -: p) by A2, A12, FINSEQ_5:42;

then 1 <= len (f -: p) by A14, NAT_1:25, XXREAL_0:2;

then len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 1;

then (len ((f -: p) /^ 1)) + 1 = len (f -: p) ;

then j <= len ((f -: p) /^ 1) by A17, A19, XREAL_1:6;

then A20: j in dom ((f -: p) /^ 1) by A18, FINSEQ_3:25;

A21: len <*((f -: p) /. 1)*> = 1 by FINSEQ_1:39;

f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by A2, FINSEQ_5:29, FINSEQ_5:47;

then ((f -: p) /^ 1) /. j = (f -: p) /. i by A17, A20, A21, FINSEQ_4:69

.= f /. i by A2, A16, FINSEQ_5:43 ;

then x in rng ((f -: p) /^ 1) by A9, A20, PARTFUN2:2;

hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def 3; :: thesis: verum

suppose
i > p .. f
; :: thesis: x in rng (Rotate (f,p))

then reconsider j = i - (p .. f) as Element of NAT by INT_1:5;

A22: j + 1 >= 1 by NAT_1:11;

i <= len f by A7, FINSEQ_3:25;

then A23: j <= (len f) - (p .. f) by XREAL_1:9;

len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50;

then j + 1 <= len (f :- p) by A23, XREAL_1:6;

then A24: j + 1 in dom (f :- p) by A22, FINSEQ_3:25;

j + (p .. f) = i ;

then f /. i = (f :- p) /. (j + 1) by A2, A24, FINSEQ_5:52;

then x in rng (f :- p) by A9, A24, PARTFUN2:2;

hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def 3; :: thesis: verum

end;A22: j + 1 >= 1 by NAT_1:11;

i <= len f by A7, FINSEQ_3:25;

then A23: j <= (len f) - (p .. f) by XREAL_1:9;

len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50;

then j + 1 <= len (f :- p) by A23, XREAL_1:6;

then A24: j + 1 in dom (f :- p) by A22, FINSEQ_3:25;

j + (p .. f) = i ;

then f /. i = (f :- p) /. (j + 1) by A2, A24, FINSEQ_5:52;

then x in rng (f :- p) by A9, A24, PARTFUN2:2;

hence x in rng (Rotate (f,p)) by A3, A6, XBOOLE_0:def 3; :: thesis: verum