let x be FinSequence of REAL ; :: thesis: for M being Matrix of REAL holds
( M = LineVec2Mx x iff ( Line M,1 = x & len M = 1 ) )
let M be Matrix of REAL ; :: thesis: ( M = LineVec2Mx x iff ( Line M,1 = x & len M = 1 ) )
thus ( M = LineVec2Mx x implies ( Line M,1 = x & len M = 1 ) ) :: thesis: ( Line M,1 = x & len M = 1 implies M = LineVec2Mx x )

proof

assume A1: M = LineVec2Mx x ; :: thesis: ( Line M,1 = x & len M = 1 )
then A2: ( width M = len x & len M = 1 ) by Def10;
then A3: dom x = Seg (width M) by FINSEQ_1:def 3;
for j being Nat st j in dom x holds
M * 1,j = x . j by A1, Def10;
hence ( Line M,1 = x & len M = 1 ) by A2, A3, MATRIX_1:def 8; :: thesis: verum

end;

assume A4: ( Line M,1 = x & len M = 1 ) ; :: thesis: M = LineVec2Mx x
then A5: ( len x = width M & ( for j being Nat st j in Seg (width M) holds
x . j = M * 1,j ) ) by MATRIX_1:def 8;
then Seg (width M) = dom x by FINSEQ_1:def 3;
hence M = LineVec2Mx x by A4, A5, Def10; :: thesis: verum