let D be non empty set ; 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; 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; ( ( 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 )
; ( MD = ColVec2Mx bD iff ( Col (MD,1) = bD & width MD = 1 ) )
thus
( MD = ColVec2Mx bD implies ( Col (MD,1) = bD & width MD = 1 ) )
( Col (MD,1) = bD & width MD = 1 implies MD = ColVec2Mx bD )
assume that
A4:
Col (MD,1) = bD
and
A5:
width MD = 1
; 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
; verum