let p be non empty FinSequence; :: thesis: <*(p . 1)*> is_a_prefix_of p

A1: now

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

end;

len p >= 1 by FINSEQ_1:20;
then len <*(p . 1)*> <= len p by FINSEQ_1:39;
then dom <*(p . 1)*> c= dom p by FINSEQ_3:30;
hence <*(p . 1)*> is_a_prefix_of p by A1, GRFUNC_1:2; :: thesis: verum