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 )

proof

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;

then reconsider C = <*x*> as Matrix of REAL by MATRIX_0:9;
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, ZFMISC_1:def 2;
hence C * (1,j) = x . j by MATRIX_0:def 5, A5; :: thesis: verum