let D be non empty set ; :: thesis: for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g /. (len g) = f /. 1 holds
f ^' g is circular
let f be non empty FinSequence of D; :: thesis: for g being non trivial FinSequence of D st g /. (len g) = f /. 1 holds
f ^' g is circular
let g be non trivial FinSequence of D; :: thesis: ( g /. (len g) = f /. 1 implies f ^' g is circular )
assume g /. (len g) = f /. 1 ; :: thesis: f ^' g is circular
hence (f ^' g) /. 1 = g /. (len g) by FINSEQ_6:155
.= (f ^' g) /. (len (f ^' g)) by FINSEQ_6:156 ;
:: according to FINSEQ_6:def 1 :: thesis: verum