let D be non empty set ; :: thesis: for f being non empty FinSequence of D st f is circular holds

f . 1 = f . (len f)

let f be non empty FinSequence of D; :: thesis: ( f is circular implies f . 1 = f . (len f) )

assume A4: f is circular ; :: thesis: f . 1 = f . (len f)

A2: 0 + 1 <= len f by NAT_1:13;

then A1: 1 in dom f by FINSEQ_3:25;

A3: len f in dom f by FINSEQ_3:25, A2;

thus f . 1 = f /. 1 by PARTFUN1:def 6, A1

.= f . (len f) by PARTFUN1:def 6, A3, A4 ; :: thesis: verum

f . 1 = f . (len f)

let f be non empty FinSequence of D; :: thesis: ( f is circular implies f . 1 = f . (len f) )

assume A4: f is circular ; :: thesis: f . 1 = f . (len f)

A2: 0 + 1 <= len f by NAT_1:13;

then A1: 1 in dom f by FINSEQ_3:25;

A3: len f in dom f by FINSEQ_3:25, A2;

thus f . 1 = f /. 1 by PARTFUN1:def 6, A1

.= f . (len f) by PARTFUN1:def 6, A3, A4 ; :: thesis: verum