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 )

A4: Col (MD,1) = bD and

A5: width MD = 1 ; :: thesis: MD = ColVec2Mx bD

A6: len MD > 0 by A1, A4, MATRIX_0:def 8;

A7: len (MD @) = 1 by A5, MATRIX_0:def 6;

1 in Seg 1 ;

then Line ((MD @),1) = bD by A4, A5, MATRIX_0:59;

then (LineVec2Mx bD) @ = (MD @) @ by A7, Th25

.= MD by A5, A6, MATRIX_0:57 ;

hence MD = ColVec2Mx bD ; :: thesis: verum

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 that
len (LineVec2Mx bD) = 1
by Th25;

then A2: dom (LineVec2Mx bD) = 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 ((LineVec2Mx bD),1) by A3, A2, MATRIX_0:58

.= bD by Th25 ;

:: thesis: width MD = 1

len MD = len bD by A3, MATRIX_0:def 2;

hence width MD = 1 by A1, A3, MATRIX_0:23; :: thesis: verum

end;then A2: dom (LineVec2Mx bD) = 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 ((LineVec2Mx bD),1) by A3, A2, MATRIX_0:58

.= bD by Th25 ;

:: thesis: width MD = 1

len MD = len bD by A3, MATRIX_0:def 2;

hence width MD = 1 by A1, A3, MATRIX_0:23; :: thesis: verum

A4: Col (MD,1) = bD and

A5: width MD = 1 ; :: thesis: MD = ColVec2Mx bD

A6: len MD > 0 by A1, A4, MATRIX_0:def 8;

A7: len (MD @) = 1 by A5, MATRIX_0:def 6;

1 in Seg 1 ;

then Line ((MD @),1) = bD by A4, A5, MATRIX_0:59;

then (LineVec2Mx bD) @ = (MD @) @ by A7, Th25

.= MD by A5, A6, MATRIX_0:57 ;

hence MD = ColVec2Mx bD ; :: thesis: verum