let M1, M2 be Matrix of COMPLEX; :: thesis: ( len M1 = len x & width M1 = 1 & ( for j being Nat st j in Seg (len x) holds
M1 . j = <*(x . j)*> ) & len M2 = len x & width M2 = 1 & ( for j being Nat st j in Seg (len x) holds
M2 . j = <*(x . j)*> ) implies M1 = M2 )
assume that
A8: len M1 = len x and
width M1 = 1 and
A9: for k being Nat st k in Seg (len x) holds
M1 . k = <*(x . k)*> and
A10: len M2 = len x and
width M2 = 1 and
A11: for k being Nat st k in Seg (len x) holds
M2 . k = <*(x . k)*> ; :: thesis: M1 = M2
A12: dom M1 = Seg (len x) by A8, FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom M1 holds
M1 . k = M2 . k

let k be Nat; :: thesis: ( k in dom M1 implies M1 . k = M2 . k )
assume A13: k in dom M1 ; :: thesis: M1 . k = M2 . k
hence M1 . k = <*(x . k)*> by A9, A12
.= M2 . k by A11, A12, A13 ;
:: thesis: verum

end;

hence M1 = M2 by A8, A10, FINSEQ_2:9; :: thesis: verum