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
A5: width A = len x and
A6: len A = 1 and
A7: for k being Nat st k in dom x holds
A * (1,k) = x . k and
A8: ( width B = len x & len B = 1 ) and
A9: for k being Nat st k in dom x holds
B * (1,k) = x . k ; :: thesis: A = B
A10: dom A = Seg 1 by A6, 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 A11: [i,j] in Indices A ; :: thesis: A * (i,j) = B * (i,j)
then i in Seg 1 by A10, ZFMISC_1:106;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:3;
then A12: i = 1 by XXREAL_0:1;
j in Seg (len x) by A5, A11, ZFMISC_1:106;
then A13: j in dom x by FINSEQ_1:def 3;
then A * (i,j) = x . j by A7, A12;
hence A * (i,j) = B * (i,j) by A9, A13, A12; :: thesis: verum

end;

hence A = B by A5, A6, A8, MATRIX_1:21; :: thesis: verum