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;
per cases ( i = 1 or ( i <= p .. f & i <> 1 ) or i > p .. f ) ;
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;
suppose that A12: i <= p .. f and
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;
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;
end;