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 )

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

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

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