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_1:24; :: 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_1:24; :: thesis: for i being Nat st i < m holds
(mConv p,m) * (i + 1),1 = p . i

now

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 Def4;
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