let p be FinSequence; :: thesis: ( len p <> 0 implies p /^ ((len p) -' 1) = <*(p . (len p))*> )
assume len p <> 0 ; :: thesis: p /^ ((len p) -' 1) = <*(p . (len p))*>
then A1: 1 <= len p by NAT_1:14;
then A2: 1 - 1 <= (len p) - 1 by XREAL_1:9;
A3: (len p) -' 1 <= len p by NAT_D:44;
then A4: len (p /^ ((len p) -' 1)) = (len p) - (((len p) + 0) -' 1) by RFINSEQ:def 1
.= (len p) - (((len p) + 0) - 1) by A1, NAT_D:37
.= 1 ;
then 1 in dom (p /^ ((len p) -' 1)) by FINSEQ_3:25;
then (p /^ ((len p) -' 1)) . 1 = p . (((len p) -' 1) + 1) by A3, RFINSEQ:def 1
.= p . (len p) by A2, NAT_D:72 ;
hence p /^ ((len p) -' 1) = <*(p . (len p))*> by A4, FINSEQ_1:40; :: thesis: verum