let p be non empty FinSequence; :: thesis: <*(p . 1)*> ^' p = p
set o = <*(p . 1)*> ^' p;
A1: (len (<*(p . 1)*> ^' p)) + 1 = (len <*(p . 1)*>) + (len p) by FINSEQ_6:139;
A2: len <*(p . 1)*> = 1 by FINSEQ_1:39;

A3: now :: thesis: for k being Nat st 1 <= k & k <= len (<*(p . 1)*> ^' p) holds
(<*(p . 1)*> ^' p) . k = p . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (<*(p . 1)*> ^' p) implies (<*(p . 1)*> ^' p) . b₁ = p . b₁ )
assume that
A4: 1 <= k and
A5: k <= len (<*(p . 1)*> ^' p) ; :: thesis: (<*(p . 1)*> ^' p) . b₁ = p . b₁

per cases ( k <= len <*(p . 1)*> or k > len <*(p . 1)*> ) ;

suppose A6: k <= len <*(p . 1)*> ; :: thesis: (<*(p . 1)*> ^' p) . b₁ = p . b₁

then k <= 1 by FINSEQ_1:39;
then A7: k = 1 by A4, XXREAL_0:1;
hence (<*(p . 1)*> ^' p) . k = <*(p . 1)*> . 1 by A6, FINSEQ_6:140
.= p . k by A7 ;
:: thesis: verum

end;

suppose k > len <*(p . 1)*> ; :: thesis: (<*(p . 1)*> ^' p) . b₁ = p . b₁

then consider i being Element of NAT such that
A8: k = (len <*(p . 1)*>) + i and
A9: 1 <= i by FINSEQ_4:84;
i < len p by A1, A2, A5, A8, NAT_1:13;
hence (<*(p . 1)*> ^' p) . k = p . k by A2, A8, A9, FINSEQ_6:141; :: thesis: verum

end;

end;

end;

(len (<*(p . 1)*> ^' p)) + 1 = 1 + (len p) by A1, FINSEQ_1:39;
hence <*(p . 1)*> ^' p = p by A3, FINSEQ_1:14; :: thesis: verum