let A, B be Matrix of REAL; :: thesis: ( len A = len x & width A = 1 & ( for j being Nat st j in dom x holds
A . j = <*(x . j)*> ) & len B = len x & width B = 1 & ( for j being Nat st j in dom x holds
B . j = <*(x . j)*> ) implies A = B )
assume that
A7: len A = len x and
width A = 1 and
A8: for k being Nat st k in dom x holds
A . k = <*(x . k)*> and
A9: len B = len x and
width B = 1 and
A10: for k being Nat st k in dom x holds
B . k = <*(x . k)*> ; :: thesis: A = B

A11: now :: thesis: for k being Nat st k in dom x holds
A . k = B . k

let k be Nat; :: thesis: ( k in dom x implies A . k = B . k )
assume A12: k in dom x ; :: thesis: A . k = B . k
hence A . k = <*(x . k)*> by A8
.= B . k by A10, A12 ;
:: thesis: verum

end;

( dom A = dom x & dom B = dom x ) by A7, A9, FINSEQ_3:29;
hence A = B by A11, FINSEQ_1:13; :: thesis: verum