reconsider n = len x as Element of NAT ;
deffunc H₁( Nat) -> set = <*(x . $1)*>;
consider C being FinSequence such that
A2: ( len C = n & ( for j being Nat st j in dom C holds
C . j = H₁(j) ) ) from FINSEQ_1:sch 2();
for y being object st y in rng C holds
ex p being FinSequence of REAL st
( y = p & len p = 1 )

proof

let y be object ; :: thesis: ( y in rng C implies ex p being FinSequence of REAL st
( y = p & len p = 1 ) )
assume y in rng C ; :: thesis: ex p being FinSequence of REAL st
( y = p & len p = 1 )
then consider z being object such that
A3: z in dom C and
A4: y = C . z by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A3;
reconsider xz = x . z as Element of REAL by XREAL_0:def 1;
len <*xz*> = 1 by FINSEQ_1:39;
hence ex p being FinSequence of REAL st
( y = p & len p = 1 ) by A2, A3, A4; :: thesis: verum

end;

then reconsider B = C as Matrix of REAL by MATRIX_0:9;
for p being FinSequence of REAL st p in rng B holds
len p = 1

proof

let p be FinSequence of REAL ; :: thesis: ( p in rng B implies len p = 1 )
assume p in rng B ; :: thesis: len p = 1
then consider i being Nat such that
A5: ( i in dom B & B . i = p ) by FINSEQ_2:10;
len <*(x . i)*> = 1 by FINSEQ_1:39;
hence len p = 1 by A2, A5; :: thesis: verum

end;

then reconsider A = B as Matrix of len B,1,REAL by MATRIX_0:def 2;
A6: Seg (len x) = dom x by FINSEQ_1:def 3;
( dom C = Seg n & width A = 1 ) by A1, A2, FINSEQ_1:def 3, MATRIX_0:23;
hence ex b₁ being Matrix of REAL st
( len b₁ = len x & width b₁ = 1 & ( for j being Nat st j in dom x holds
b₁ . j = <*(x . j)*> ) ) by A2, A6; :: thesis: verum