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_1:24 ;
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:106;
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:3;
then reconsider k = i - 1 as Nat by NAT_1:20;
A8: j in Seg (width (mConv a,m)) by A5, ZFMISC_1:106;
then A9: 1 <= j by FINSEQ_1:3;
j in Seg 1 by A1, A8, Th28;
then A10: j <= 1 by FINSEQ_1:3;
k + 1 <= m by A7, FINSEQ_1:3;
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_1:24 ;
hence mConv a,m = M by A2, A4, MATRIX_1:21; :: thesis: verum