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 )

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_0:51;

1 in Seg 1 ;

then md . 1 = bD by A2, MATRIX_0:52;

hence MD = LineVec2Mx bD by A3, FINSEQ_1:40; :: thesis: verum

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

assume that
1 in Seg 1
;

then A1: Line ((LineVec2Mx bD),1) = (LineVec2Mx bD) . 1 by MATRIX_0:52;

assume MD = LineVec2Mx bD ; :: thesis: ( Line (MD,1) = bD & len MD = 1 )

hence ( Line (MD,1) = bD & len MD = 1 ) by A1, FINSEQ_1:40; :: thesis: verum

end;then A1: Line ((LineVec2Mx bD),1) = (LineVec2Mx bD) . 1 by MATRIX_0:52;

assume MD = LineVec2Mx bD ; :: thesis: ( Line (MD,1) = bD & len MD = 1 )

hence ( Line (MD,1) = bD & len MD = 1 ) by A1, FINSEQ_1:40; :: thesis: verum

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_0:51;

1 in Seg 1 ;

then md . 1 = bD by A2, MATRIX_0:52;

hence MD = LineVec2Mx bD by A3, FINSEQ_1:40; :: thesis: verum