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 /. (len f))*>
let f be FinSequence of D; :: thesis: ( f just_once_values f /. (len f) implies f :- (f /. (len f)) = <*(f /. (len f))*> )
assume A1: f just_once_values f /. (len f) ; :: thesis: f :- (f /. (len f)) = <*(f /. (len f))*>
thus f :- (f /. (len f)) = <*(f /. (len f))*> ^ (f /^ ((f /. (len f)) .. f)) by FINSEQ_5:def 2
.= <*(f /. (len f))*> ^ (f /^ (len f)) by A1, Th1
.= <*(f /. (len f))*> ^ {} by RFINSEQ:27
.= <*(f /. (len f))*> by FINSEQ_1:34 ; :: thesis: verum