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: for j being Nat st j in dom x holds
M * (1,j) = x . j by Def10;
A3: width M = len x by A1, Def10;
then dom x = Seg (width M) by FINSEQ_1:def 3;
hence ( Line (M,1) = x & len M = 1 ) by A1, A3, A2, Def10, MATRIX_0:def 7; :: thesis: verum
end;
assume that
A4: Line (M,1) = x and
A5: len M = 1 ; :: thesis: M = LineVec2Mx x
A6: for j being Nat st j in Seg (width M) holds
x . j = M * (1,j) by A4, MATRIX_0:def 7;
A7: len x = width M by A4, MATRIX_0:def 7;
then Seg (width M) = dom x by FINSEQ_1:def 3;
hence M = LineVec2Mx x by A5, A7, A6, Def10; :: thesis: verum