let i be Nat; :: thesis: for f being FinSequence st i + 1 = len f holds
f /^ i = <*(f . (len f))*>
let f be FinSequence; :: 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 1
.= 1 by A1 ;
then A3: 1 in dom (f /^ i) by FINSEQ_3:25;
thus f /^ i = <*((f /^ i) . 1)*> by A2, Th14
.= <*(f . (len f))*> by A1, A3, Th27 ; :: thesis: verum