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 )
assume A2: for i being Nat st i < m holds
M * (i + 1),1 = a . i ; :: thesis: mConv a,m = M
A3: len (mConv a,m) = m by A1, Th28
.= len M by A1, MATRIX_1:24 ;
A4: width (mConv a,m) = 1 by A1, Th28
.= width M by A1, MATRIX_1:24 ;
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:106;
A7: j in Seg (width (mConv a,m)) by A5, ZFMISC_1:106;
len (mConv a,m) = m by A1, Th28;
then A8: i in Seg m by A6, FINSEQ_1:def 3;
then A9: 0 < i by FINSEQ_1:3;
j in Seg 1 by A1, A7, Th28;
then A10: ( 1 <= j & j <= 1 ) by FINSEQ_1:3;
reconsider k = i - 1 as Nat by A9, NAT_1:20;
k + 1 <= m by A8, FINSEQ_1:3;
then A11: k < m by NAT_1:13;
then M * (k + 1),1 = a . k by A2
.= (mConv a,m) * (k + 1),1 by A11, Th28
.= (mConv a,m) * i,j by A10, XXREAL_0:1 ;
hence (mConv a,m) * i,j = M * i,j by A10, XXREAL_0:1; :: thesis: verum

end;

hence mConv a,m = M by A3, A4, MATRIX_1:21; :: thesis: verum