let D be non empty set ; :: thesis: for bD being FinSequence of D
for MD being Matrix of D st ( len MD <> 0 or len bD <> 0 ) holds
( MD = ColVec2Mx bD iff ( Col MD,1 = bD & width MD = 1 ) )
let bD be FinSequence of D; :: thesis: for MD being Matrix of D st ( len MD <> 0 or len bD <> 0 ) holds
( MD = ColVec2Mx bD iff ( Col MD,1 = bD & width MD = 1 ) )
let MD be Matrix of D; :: thesis: ( ( len MD <> 0 or len bD <> 0 ) implies ( MD = ColVec2Mx bD iff ( Col MD,1 = bD & width MD = 1 ) ) )
assume A1: ( len MD <> 0 or len bD <> 0 ) ; :: thesis: ( MD = ColVec2Mx bD iff ( Col MD,1 = bD & width MD = 1 ) )
thus ( MD = ColVec2Mx bD implies ( Col MD,1 = bD & width MD = 1 ) ) :: thesis: ( Col MD,1 = bD & width MD = 1 implies MD = ColVec2Mx bD )

proof

assume A2: MD = ColVec2Mx bD ; :: thesis: ( Col MD,1 = bD & width MD = 1 )
len (LineVec2Mx bD) = 1 by Th25;
then ( dom (LineVec2Mx bD) = Seg 1 & 1 in Seg 1 ) by FINSEQ_1:def 3;
hence Col MD,1 = Line (LineVec2Mx bD),1 by A2, MATRIX_2:16
.= bD by Th25 ;
:: thesis: width MD = 1
A3: len MD = len bD by A2, MATRIX_1:def 3;
then len MD > 0 by A1;
hence width MD = 1 by A2, A3, MATRIX_1:24; :: thesis: verum

end;

assume A4: ( Col MD,1 = bD & width MD = 1 ) ; :: thesis: MD = ColVec2Mx bD
then A5: ( len bD = len MD & len (MD @ ) = 1 ) by MATRIX_1:def 7, MATRIX_1:def 9;
then A6: len MD > 0 by A1;
1 in Seg 1 ;
then Line (MD @ ),1 = bD by A4, MATRIX_2:17;
then (LineVec2Mx bD) @ = (MD @ ) @ by A5, Th25
.= MD by A4, A6, MATRIX_2:15 ;
hence MD = ColVec2Mx bD ; :: thesis: verum