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
len () = 1 by Th25;
then A2: dom () = Seg 1 by FINSEQ_1:def 3;
assume A3: MD = ColVec2Mx bD ; :: thesis: ( Col (MD,1) = bD & width MD = 1 )
1 in Seg 1 ;
hence Col (MD,1) = Line ((),1) by
.= bD by Th25 ;
:: thesis: width MD = 1
len MD = len bD by ;
hence width MD = 1 by ; :: thesis: verum
end;
assume that
A4: Col (MD,1) = bD and
A5: width MD = 1 ; :: thesis: MD = ColVec2Mx bD
A6: len MD > 0 by ;
A7: len (MD @) = 1 by ;
1 in Seg 1 ;
then Line ((MD @),1) = bD by ;
then () @ = (MD @) @ by
.= MD by ;
hence MD = ColVec2Mx bD ; :: thesis: verum