let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>
let D be non empty set ; :: thesis: for f being FinSequence of D st i + 1 = len f holds
f /^ i = <*(f /. (len f))*>
let f be FinSequence of D; :: thesis: ( i + 1 = len f implies f /^ i = <*(f /. (len f))*> )
assume A1: i + 1 = len f ; :: thesis: f /^ i = <*(f /. (len f))*>
then i <= len f by NAT_1:11;
then A2: len (f /^ i) = (len f) - i by RFINSEQ:def 2
.= 1 by A1 ;
then A3: 1 in dom (f /^ i) by FINSEQ_3:27;
thus f /^ i = <*((f /^ i) /. 1)*> by A2, Th15
.= <*(f /. (len f))*> by A1, A3, Th30 ; :: thesis: verum