let A, B be Matrix of REAL; :: thesis: ( width A = len x & len A = 1 & ( for j being Nat st j in dom x holds
A * (1,j) = x . j ) & width B = len x & len B = 1 & ( for j being Nat st j in dom x holds
B * (1,j) = x . j ) implies A = B )
assume that
A6: width A = len x and
A7: len A = 1 and
A8: for k being Nat st k in dom x holds
A * (1,k) = x . k and
A9: ( width B = len x & len B = 1 ) and
A10: for k being Nat st k in dom x holds
B * (1,k) = x . k ; :: thesis: A = B
A11: dom A = Seg 1 by A7, FINSEQ_1:def 3;
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
assume A12: [i,j] in Indices A ; :: thesis: A * (i,j) = B * (i,j)
then i in Seg 1 by A11, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A13: i = 1 by XXREAL_0:1;
j in Seg (len x) by A6, A12, ZFMISC_1:87;
then A14: j in dom x by FINSEQ_1:def 3;
then A * (i,j) = x . j by A8, A13;
hence A * (i,j) = B * (i,j) by A10, A14, A13; :: thesis: verum

end;

hence A = B by A6, A7, A9, MATRIX_0:21; :: thesis: verum