let A, B be Matrix of REAL; ( 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
; 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;
( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
assume A12:
[i,j] in Indices A
;
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;
verum
end;
hence
A = B
by A6, A7, A9, MATRIX_0:21; verum