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

(mConv (p,m)) * ((i + 1),1) = p . i ; :: thesis: verum

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

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

(mConv (p,m)) * ((i + 1),1) = p . i ; :: thesis: verum