let D be non empty set ; :: thesis: for f being FinSequence of D st f just_once_values f /. (len f) holds

(f /. (len f)) .. f = len f

let f be FinSequence of D; :: thesis: ( f just_once_values f /. (len f) implies (f /. (len f)) .. f = len f )

assume A1: f just_once_values f /. (len f) ; :: thesis: (f /. (len f)) .. f = len f

then reconsider f9 = f as non empty FinSequence of D by FINSEQ_4:5, RELAT_1:38;

((f /. (len f)) .. f) + 1 = ((f /. (len f)) .. f) + (((Rev f9) /. 1) .. (Rev f9)) by Th43

.= ((f /. (len f)) .. f) + ((f /. (len f)) .. (Rev f)) by FINSEQ_5:65

.= (len f) + 1 by A1, Th37 ;

hence (f /. (len f)) .. f = len f ; :: thesis: verum

(f /. (len f)) .. f = len f

let f be FinSequence of D; :: thesis: ( f just_once_values f /. (len f) implies (f /. (len f)) .. f = len f )

assume A1: f just_once_values f /. (len f) ; :: thesis: (f /. (len f)) .. f = len f

then reconsider f9 = f as non empty FinSequence of D by FINSEQ_4:5, RELAT_1:38;

((f /. (len f)) .. f) + 1 = ((f /. (len f)) .. f) + (((Rev f9) /. 1) .. (Rev f9)) by Th43

.= ((f /. (len f)) .. f) + ((f /. (len f)) .. (Rev f)) by FINSEQ_5:65

.= (len f) + 1 by A1, Th37 ;

hence (f /. (len f)) .. f = len f ; :: thesis: verum