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 ;
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 ;
then ( len <*x*> = 1 & C is Matrix of 1, len x,REAL ) by ;
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 ;
hence C * (1,j) = x . j by ; :: thesis: verum