let m be Nat; :: thesis: ( m > 0 implies for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M )
assume A1: m > 0 ; :: thesis: for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
let L be non empty ZeroStr ; :: thesis: for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
let a be AlgSequence of L; :: thesis: for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) holds
mConv (a,m) = M
let M be Matrix of m,1,L; :: thesis: ( ( for i being Nat st i < m holds
M * ((i + 1),1) = a . i ) implies mConv (a,m) = M )
A2: width (mConv (a,m)) = 1 by A1, Th28
.= width M by A1, MATRIX_0:23 ;
assume A3: for i being Nat st i < m holds
M * ((i + 1),1) = a . i ; :: thesis: mConv (a,m) = M
A4: for i, j being Nat st [i,j] in Indices (mConv (a,m)) holds
(mConv (a,m)) * (i,j) = M * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (mConv (a,m)) implies (mConv (a,m)) * (i,j) = M * (i,j) )
assume A5: [i,j] in Indices (mConv (a,m)) ; :: thesis: (mConv (a,m)) * (i,j) = M * (i,j)
then A6: i in dom (mConv (a,m)) by ZFMISC_1:87;
len (mConv (a,m)) = m by A1, Th28;
then A7: i in Seg m by A6, FINSEQ_1:def 3;
then 0 < i by FINSEQ_1:1;
then reconsider k = i - 1 as Nat by NAT_1:20;
A8: j in Seg (width (mConv (a,m))) by A5, ZFMISC_1:87;
then A9: 1 <= j by FINSEQ_1:1;
j in Seg 1 by A1, A8, Th28;
then A10: j <= 1 by FINSEQ_1:1;
k + 1 <= m by A7, FINSEQ_1:1;
then A11: k < m by NAT_1:13;
then M * ((k + 1),1) = a . k by A3
.= (mConv (a,m)) * ((k + 1),1) by A11, Th28
.= (mConv (a,m)) * (i,j) by A9, A10, XXREAL_0:1 ;
hence (mConv (a,m)) * (i,j) = M * (i,j) by A9, A10, XXREAL_0:1; :: thesis: verum

end;

len (mConv (a,m)) = m by A1, Th28
.= len M by A1, MATRIX_0:23 ;
hence mConv (a,m) = M by A2, A4, MATRIX_0:21; :: thesis: verum