let m be Nat; :: thesis: ( m > 0 implies for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) ) )
assume A1: m > 0 ; :: thesis: for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
let L be non empty ZeroStr ; :: thesis: for p being AlgSequence of L holds
( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
let p be AlgSequence of L; :: thesis: ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
set q = mConv (p,m);
thus len (mConv (p,m)) = m by A1, MATRIX_0:23; :: thesis: ( width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ) )
thus width (mConv (p,m)) = 1 by A1, MATRIX_0:23; :: thesis: for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i

now :: thesis: for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i

let i be Nat; :: thesis: ( i < m implies (mConv (p,m)) * ((i + 1),1) = p . i )
assume i < m ; :: thesis: (mConv (p,m)) * ((i + 1),1) = p . i
then ( 0 + 1 <= i + 1 & i + 1 <= m ) by NAT_1:13;
then (mConv (p,m)) * ((i + 1),1) = p . ((i + 1) - 1) by Def3;
hence (mConv (p,m)) * ((i + 1),1) = p . i ; :: thesis: verum

end;

hence for i being Nat st i < m holds
(mConv (p,m)) * ((i + 1),1) = p . i ; :: thesis: verum