let D be non empty set ; :: thesis: for pf being FinSequence of D holds Line (<*pf*>,1) = pf
let pf be FinSequence of D; :: thesis: Line (<*pf*>,1) = pf
1 in Seg 1 by FINSEQ_1:1;
then Line (<*pf*>,1) = <*pf*> . 1 by MATRIX_0:52;
hence Line (<*pf*>,1) = pf by FINSEQ_1:40; :: thesis: verum