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)

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

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;

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

hence x in rng (f /^ 1) ; :: thesis: verum

end;

end;