let p be non empty FinSequence; :: thesis: <*(p . 1)*> is_a_prefix_of p
len p >= 1 by FINSEQ_1:28;
then len <*(p . 1)*> <= len p by FINSEQ_1:56;
then A1: dom <*(p . 1)*> c= dom p by FINSEQ_3:32;

now

let x be set ; :: thesis: ( x in dom <*(p . 1)*> implies <*(p . 1)*> . x = p . x )
assume A2: x in dom <*(p . 1)*> ; :: thesis: <*(p . 1)*> . x = p . x
dom <*(p . 1)*> = Seg 1 by FINSEQ_1:def 8;
then x = 1 by A2, FINSEQ_1:4, TARSKI:def 1;
hence <*(p . 1)*> . x = p . x by FINSEQ_1:def 8; :: thesis: verum

end;

hence <*(p . 1)*> is_a_prefix_of p by A1, GRFUNC_1:8; :: thesis: verum