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)

.= len M by A1, MATRIX_0:23 ;

hence mConv (a,m) = M by A2, A4, MATRIX_0:21; :: thesis: verum

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

len (mConv (a,m)) =
m
by A1, Th28
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;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

.= len M by A1, MATRIX_0:23 ;

hence mConv (a,m) = M by A2, A4, MATRIX_0:21; :: thesis: verum