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

proof

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

end;

then reconsider M2 = M3 as Matrix of COMPLEX by MATRIX_0:9;
for p being FinSequence of COMPLEX st p in rng M2 holds
len p = 1

proof

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

end;

then reconsider M1 = M2 as Matrix of len M2,1,COMPLEX by MATRIX_0:def 2;
take M2 ; :: thesis: ( len M2 = len x & width M2 = 1 & ( for j being Nat st j in Seg (len x) holds
M2 . j = <*(x . j)*> ) )
A7: dom M3 = Seg n by A2, FINSEQ_1:def 3;
width M1 = 1 by A1, A2, MATRIX_0:23;
hence ( len M2 = len x & width M2 = 1 & ( for j being Nat st j in Seg (len x) holds
M2 . j = <*(x . j)*> ) ) by A2, A7; :: thesis: verum