let D be non empty set ; :: thesis: for bD being FinSequence of D
for MD being Matrix of D holds
( MD = LineVec2Mx bD iff ( Line MD,1 = bD & len MD = 1 ) )
let bD be FinSequence of D; :: thesis: for MD being Matrix of D holds
( MD = LineVec2Mx bD iff ( Line MD,1 = bD & len MD = 1 ) )
let MD be Matrix of D; :: thesis: ( MD = LineVec2Mx bD iff ( Line MD,1 = bD & len MD = 1 ) )
thus ( MD = LineVec2Mx bD implies ( Line MD,1 = bD & len MD = 1 ) ) :: thesis: ( Line MD,1 = bD & len MD = 1 implies MD = LineVec2Mx bD )

proof

1 in Seg 1 ;
then A1: Line (LineVec2Mx bD),1 = (LineVec2Mx bD) . 1 by MATRIX_2:10;
assume MD = LineVec2Mx bD ; :: thesis: ( Line MD,1 = bD & len MD = 1 )
hence ( Line MD,1 = bD & len MD = 1 ) by A1, FINSEQ_1:57; :: thesis: verum

end;

assume that
A2: Line MD,1 = bD and
A3: len MD = 1 ; :: thesis: MD = LineVec2Mx bD
reconsider md = MD as Matrix of 1, width MD,D by A3, MATRIX_2:7;
1 in Seg 1 ;
then md . 1 = bD by A2, MATRIX_2:10;
hence MD = LineVec2Mx bD by A3, FINSEQ_1:57; :: thesis: verum