let x be FinSequence of REAL ; :: thesis: for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col M,1 = x & width M = 1 ) )
let M be Matrix of REAL ; :: thesis: ( len x > 0 implies ( M = ColVec2Mx x iff ( Col M,1 = x & width M = 1 ) ) )
consider n being Nat such that
A1: for x being set st x in rng M holds
ex s2 being FinSequence st
( s2 = x & len s2 = n ) by MATRIX_1:def 1;
assume A2: len x > 0 ; :: thesis: ( M = ColVec2Mx x iff ( Col M,1 = x & width M = 1 ) )
thus ( M = ColVec2Mx x implies ( Col M,1 = x & width M = 1 ) ) :: thesis: ( Col M,1 = x & width M = 1 implies M = ColVec2Mx x )

proof

assume A3: M = ColVec2Mx x ; :: thesis: ( Col M,1 = x & width M = 1 )
then A4: width M = 1 by A2, Def9;
A5: len M = len x by A2, A3, Def9;
then A6: dom M = dom x by FINSEQ_3:31;
for j being Nat st j in dom M holds
x . j = M * j,1

proof

let j be Nat; :: thesis: ( j in dom M implies x . j = M * j,1 )
assume A7: j in dom M ; :: thesis: x . j = M * j,1
then reconsider j = j as Element of NAT ;
A8: M . j = <*(x . j)*> by A2, A3, A6, A7, Def9;
then reconsider q = M . j as FinSequence of REAL ;
A9: q . 1 = x . j by A8, FINSEQ_1:57;
1 in Seg (width M) by A4, FINSEQ_1:3;
then [j,1] in Indices M by A7, ZFMISC_1:106;
hence x . j = M * j,1 by A9, MATRIX_1:def 6; :: thesis: verum

end;

hence ( Col M,1 = x & width M = 1 ) by A2, A3, A5, Def9, MATRIX_1:def 9; :: thesis: verum

end;

assume that
A10: Col M,1 = x and
A11: width M = 1 ; :: thesis: M = ColVec2Mx x
A12: len x = len M by A10, MATRIX_1:def 9;
then consider s being FinSequence such that
A13: s in rng M and
A14: len s = 1 by A2, A11, MATRIX_1:def 4;
A15: dom x = dom M by A12, FINSEQ_3:31;
A16: ex s2 being FinSequence st
( s2 = s & len s2 = n ) by A13, A1;
for j being Nat st j in dom x holds
M . j = <*(x . j)*>

proof

let j be Nat; :: thesis: ( j in dom x implies M . j = <*(x . j)*> )
assume A17: j in dom x ; :: thesis: M . j = <*(x . j)*>
then M . j in rng M by A15, FUNCT_1:def 5;
then A18: ex s3 being FinSequence st
( s3 = M . j & len s3 = 1 ) by A14, A1, A16;
1 in Seg (width M) by A11, FINSEQ_1:3;
then [j,1] in Indices M by A15, A17, ZFMISC_1:106;
then A19: ex p being FinSequence of REAL st
( p = M . j & M * j,1 = p . 1 ) by MATRIX_1:def 6;
x . j = M * j,1 by A10, A15, A17, MATRIX_1:def 9;
hence M . j = <*(x . j)*> by A19, A18, FINSEQ_1:57; :: thesis: verum

end;

hence M = ColVec2Mx x by A2, A11, A12, Def9; :: thesis: verum