deffunc H₁( Nat) -> Element of 1 -tuples_on COMPLEX = <*(x . $1)*>;
reconsider n = len x as Element of NAT ;
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();
A3: dom M3 = Seg n by A2, FINSEQ_1:def 3;
for y being set st y in rng M3 holds
ex p being FinSequence of COMPLEX st
( y = p & len p = 1 )

proof

let y be set ; :: 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 set such that
A4: ( z in dom M3 & y = M3 . z ) by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A4;
len <*(x . z)*> = 1 by FINSEQ_1:56;
hence ex p being FinSequence of COMPLEX st
( y = p & len p = 1 ) by A2, A4; :: thesis: verum

end;

then reconsider M2 = M3 as Matrix of COMPLEX by MATRIX_1:9;
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)*> ) )
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
A6: i in dom M2 and
A7: M2 . i = p by FINSEQ_2:11;
len <*(x . i)*> = 1 by FINSEQ_1:56;
hence len p = 1 by A2, A7, A6; :: thesis: verum

end;

then reconsider M1 = M2 as Matrix of len M2,1, COMPLEX by MATRIX_1:def 3;
width M1 = 1 by A1, A2, MATRIX_1:24;
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, A3; :: thesis: verum