set B = <*x*>;

A1: rng <*x*> = {x} by FINSEQ_1:39;

for y being object st y in rng <*x*> holds

ex p being FinSequence of REAL st

( y = p & len p = len x )

take C ; :: thesis: ( width C = len x & len C = 1 & ( for j being Nat st j in dom x holds

C * (1,j) = x . j ) )

A2: len <*x*> = 1 by FINSEQ_1:39;

then dom C = Seg 1 by FINSEQ_1:def 3;

then A3: 1 in dom C by FINSEQ_1:1;

for p being FinSequence of REAL st p in rng C holds

len p = len x by A1, TARSKI:def 1;

then ( len <*x*> = 1 & C is Matrix of 1, len x,REAL ) by A2, MATRIX_0:def 2;

hence A4: width C = len x by MATRIX_0:20; :: thesis: ( len C = 1 & ( for j being Nat st j in dom x holds

C * (1,j) = x . j ) )

thus len C = 1 by FINSEQ_1:40; :: thesis: for j being Nat st j in dom x holds

C * (1,j) = x . j

let j be Nat; :: thesis: ( j in dom x implies C * (1,j) = x . j )

A5: x . j in REAL by XREAL_0:def 1;

assume j in dom x ; :: thesis: C * (1,j) = x . j

then j in Seg (len x) by FINSEQ_1:def 3;

then ( <*x*> . 1 = x & [1,j] in Indices C ) by A4, A3, FINSEQ_1:40, ZFMISC_1:def 2;

hence C * (1,j) = x . j by MATRIX_0:def 5, A5; :: thesis: verum

A1: rng <*x*> = {x} by FINSEQ_1:39;

for y being object st y in rng <*x*> holds

ex p being FinSequence of REAL st

( y = p & len p = len x )

proof

then reconsider C = <*x*> as Matrix of REAL by MATRIX_0:9;
let y be object ; :: thesis: ( y in rng <*x*> implies ex p being FinSequence of REAL st

( y = p & len p = len x ) )

assume y in rng <*x*> ; :: thesis: ex p being FinSequence of REAL st

( y = p & len p = len x )

then y = x by A1, TARSKI:def 1;

hence ex p being FinSequence of REAL st

( y = p & len p = len x ) ; :: thesis: verum

end;( y = p & len p = len x ) )

assume y in rng <*x*> ; :: thesis: ex p being FinSequence of REAL st

( y = p & len p = len x )

then y = x by A1, TARSKI:def 1;

hence ex p being FinSequence of REAL st

( y = p & len p = len x ) ; :: thesis: verum

take C ; :: thesis: ( width C = len x & len C = 1 & ( for j being Nat st j in dom x holds

C * (1,j) = x . j ) )

A2: len <*x*> = 1 by FINSEQ_1:39;

then dom C = Seg 1 by FINSEQ_1:def 3;

then A3: 1 in dom C by FINSEQ_1:1;

for p being FinSequence of REAL st p in rng C holds

len p = len x by A1, TARSKI:def 1;

then ( len <*x*> = 1 & C is Matrix of 1, len x,REAL ) by A2, MATRIX_0:def 2;

hence A4: width C = len x by MATRIX_0:20; :: thesis: ( len C = 1 & ( for j being Nat st j in dom x holds

C * (1,j) = x . j ) )

thus len C = 1 by FINSEQ_1:40; :: thesis: for j being Nat st j in dom x holds

C * (1,j) = x . j

let j be Nat; :: thesis: ( j in dom x implies C * (1,j) = x . j )

A5: x . j in REAL by XREAL_0:def 1;

assume j in dom x ; :: thesis: C * (1,j) = x . j

then j in Seg (len x) by FINSEQ_1:def 3;

then ( <*x*> . 1 = x & [1,j] in Indices C ) by A4, A3, FINSEQ_1:40, ZFMISC_1:def 2;

hence C * (1,j) = x . j by MATRIX_0:def 5, A5; :: thesis: verum