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 object st x in rng M holds
ex s2 being FinSequence st
( s2 = x & len s2 = n ) by MATRIX_0: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:29;
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) )
reconsider xj = x . j as Element of REAL by XREAL_0:def 1;
assume A7: j in dom M ; :: thesis: x . j = M * (j,1)
then reconsider j = j as Element of NAT ;
A8: M . j = <*xj*> by A2, A3, A6, A7, Def9;
then reconsider q = M . j as FinSequence of REAL ;
A9: q . 1 = xj by A8;
1 in Seg (width M) by A4, FINSEQ_1:1;
then [j,1] in Indices M by A7, ZFMISC_1:87;
hence x . j = M * (j,1) by A9, MATRIX_0:def 5; :: thesis: verum

end;

hence ( Col (M,1) = x & width M = 1 ) by A2, A3, A5, Def9, MATRIX_0:def 8; :: 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_0:def 8;
then consider s being FinSequence such that
A13: s in rng M and
A14: len s = 1 by A2, A11, MATRIX_0:def 3;
A15: dom x = dom M by A12, FINSEQ_3:29;
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 3;
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:1;
then [j,1] in Indices M by A15, A17, ZFMISC_1:87;
then A19: ex p being FinSequence of REAL st
( p = M . j & M * (j,1) = p . 1 ) by MATRIX_0:def 5;
x . j = M * (j,1) by A10, A15, A17, MATRIX_0:def 8;
hence M . j = <*(x . j)*> by A19, A18, FINSEQ_1:40; :: thesis: verum

end;

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