let D be non empty set ; :: thesis: for f being non trivial circular FinSequence of D holds rng (f /^ 1) = rng f

let f be non trivial circular FinSequence of D; :: thesis: rng (f /^ 1) = rng f

thus rng (f /^ 1) c= rng f by FINSEQ_5:33; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (f /^ 1)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in rng (f /^ 1) )

f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29;

then A1: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;

assume A2: x in rng f ; :: thesis: x in rng (f /^ 1)

let f be non trivial circular FinSequence of D; :: thesis: rng (f /^ 1) = rng f

thus rng (f /^ 1) c= rng f by FINSEQ_5:33; :: according to XBOOLE_0:def 10 :: thesis: rng f c= rng (f /^ 1)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in rng (f /^ 1) )

f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29;

then A1: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:31;

assume A2: x in rng f ; :: thesis: x in rng (f /^ 1)

per cases
( x in rng <*(f /. 1)*> or x in rng (f /^ 1) )
by A1, A2, XBOOLE_0:def 3;

end;

suppose
x in rng <*(f /. 1)*>
; :: thesis: x in rng (f /^ 1)

then
x in {(f /. 1)}
by FINSEQ_1:39;

then x = f /. 1 by TARSKI:def 1;

then A3: x = f /. (len f) by Def1A;

A4: len f >= 1 + 1 by NAT_D:60;

then len f >= 1 by XXREAL_0:2;

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

then 1 <= len (f /^ 1) by A4, XREAL_1:19;

then A6: len (f /^ 1) in dom (f /^ 1) by FINSEQ_3:25;

(len (f /^ 1)) + 1 = len f by A5;

then x = (f /^ 1) /. (len (f /^ 1)) by A3, A6, FINSEQ_5:27;

hence x in rng (f /^ 1) by A6, PARTFUN2:2; :: thesis: verum

end;then x = f /. 1 by TARSKI:def 1;

then A3: x = f /. (len f) by Def1A;

A4: len f >= 1 + 1 by NAT_D:60;

then len f >= 1 by XXREAL_0:2;

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

then 1 <= len (f /^ 1) by A4, XREAL_1:19;

then A6: len (f /^ 1) in dom (f /^ 1) by FINSEQ_3:25;

(len (f /^ 1)) + 1 = len f by A5;

then x = (f /^ 1) /. (len (f /^ 1)) by A3, A6, FINSEQ_5:27;

hence x in rng (f /^ 1) by A6, PARTFUN2:2; :: thesis: verum