let D be non empty set ; :: thesis: for f being FinSequence of D st f just_once_values f /. (len f) holds
f -: (f /. (len f)) = f
let f be FinSequence of D; :: thesis: ( f just_once_values f /. (len f) implies f -: (f /. (len f)) = f )
assume A1: f just_once_values f /. (len f) ; :: thesis: f -: (f /. (len f)) = f
thus f -: (f /. (len f)) = f | ((f /. (len f)) .. f) by FINSEQ_5:def 1
.= f | (len f) by A1, Th1
.= f by FINSEQ_1:58 ; :: thesis: verum