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_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;
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_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