set f = m1 * m2;
ex n being Nat st
for i being Nat st i >= n holds
(m1 * m2) . i = 0. L

proof

take (len m1) + 1 ; :: thesis: for i being Nat st i >= (len m1) + 1 holds
(m1 * m2) . i = 0. L

now :: thesis: for i being Nat st i >= (len m1) + 1 holds
0. L = (m1 * m2) . i

let i be Nat; :: thesis: ( i >= (len m1) + 1 implies 0. L = (m1 * m2) . i )
assume i >= (len m1) + 1 ; :: thesis: 0. L = (m1 * m2) . i
then i > len m1 by NAT_1:13;
then m1 . i = 0. L by ALGSEQ_1:8;
hence 0. L = (m1 . i) * (m2 . i)
.= (m1 * m2) . i by LOPBAN_3:def 7 ;
:: thesis: verum

end;

hence for i being Nat st i >= (len m1) + 1 holds
(m1 * m2) . i = 0. L ; :: thesis: verum

end;

hence m1 * m2 is finite-Support by ALGSEQ_1:def 1; :: thesis: verum