set B = <*x*>;
A1: ( len <*x*> = 1 & rng <*x*> = {x} ) by FINSEQ_1:56;
A2: ( len <*x*> = 1 & <*x*> . 1 = x ) by FINSEQ_1:57;
for y being set st y in rng <*x*> holds
ex p being FinSequence of REAL st
( y = p & len p = len x )

proof

let y be set ; :: 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_1: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 ) )
for p being FinSequence of REAL st p in rng C holds
len p = len x by A1, TARSKI:def 1;
then C is Matrix of 1, len x, REAL by A1, MATRIX_1:def 3;
hence A3: width C = len x by A2, MATRIX_1: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:57; :: 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 )
assume A4: j in dom x ; :: thesis: C * 1,j = x . j
dom C = Seg 1 by A1, FINSEQ_1:def 3;
then A5: 1 in dom C by FINSEQ_1:3;
j in Seg (len x) by A4, FINSEQ_1:def 3;
then A6: [1,j] in Indices C by A3, A5, ZFMISC_1:def 2;
thus C * 1,j = x . j by A2, A6, MATRIX_1:def 6; :: thesis: verum