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

hence A = B by A11, FINSEQ_1:13; :: thesis: verum

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

( dom A = dom x & dom B = dom x )
by A7, A9, FINSEQ_3:29;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;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

hence A = B by A11, FINSEQ_1:13; :: thesis: verum