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 (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;
assume that
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