let D be non empty set ; :: thesis: for g being circular FinSequence of D
for p being Element of D st p in rng g & len g > 1 holds
p .. g < len g
let g be circular FinSequence of D; :: thesis: for p being Element of D st p in rng g & len g > 1 holds
p .. g < len g
let p be Element of D; :: thesis: ( p in rng g & len g > 1 implies p .. g < len g )
assume that
A1: p in rng g and
A2: len g > 1 and
A3: p .. g >= len g ; :: thesis: contradiction
p .. g <= len g by A1, FINSEQ_4:21;
then p .. g = len g by A3, XXREAL_0:1;
then A4: p = g /. (len g) by A1, FINSEQ_5:38
.= g /. 1 by FINSEQ_6:def 1 ;
not g is empty by A2, CARD_1:27;
hence contradiction by A2, A3, A4, FINSEQ_6:43; :: thesis: verum