let D be non empty set ; :: thesis: for pf being FinSequence of D holds Col ((<*pf*> @),1) = pf
let pf be FinSequence of D; :: thesis: Col ((<*pf*> @),1) = pf
len <*pf*> = 1 by FINSEQ_1:39;
then dom <*pf*> = Seg 1 by FINSEQ_1:def 3;
then Col ((<*pf*> @),1) = Line (<*pf*>,1) by FINSEQ_1:1, MATRIX_0:58;
hence Col ((<*pf*> @),1) = pf by Th72; :: thesis: verum