deffunc H₁( Element of Bags n, Element of Bags n) -> set = n + L;
set D = { H₁(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } ;
A1: Support q is finite by Def5;
A2: Support (p *' q) c= { H₁(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }

proof

let x9 be object ; :: according to TARSKI:def 3 :: thesis: ( not x9 in Support (p *' q) or x9 in { H₁(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } )
assume A3: x9 in Support (p *' q) ; :: thesis: x9 in { H₁(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }
then reconsider b = x9 as Element of Bags n ;
consider s being FinSequence of the carrier of L such that
A4: (p *' q) . b = Sum s and
A5: len s = len (decomp b) and
A6: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by Def10;
(p *' q) . b <> 0. L by A3, Def4;
then consider k being Nat such that
A7: k in dom s and
A8: s /. k <> 0. L by A4, MATRLIN:11;
consider b1, b2 being bag of n such that
A9: (decomp b) /. k = <*b1,b2*> and
A10: s /. k = (p . b1) * (q . b2) by A6, A7;
A11: b1 in Bags n by PRE_POLY:def 12;
A12: b2 in Bags n by PRE_POLY:def 12;
q . b2 <> 0. L by A8, A10;
then A13: b2 in Support q by A12, Def4;
p . b1 <> 0. L by A8, A10;
then A14: b1 in Support p by A11, Def4;
k in dom (decomp b) by A5, A7, FINSEQ_3:29;
then consider b19, b29 being bag of n such that
A15: (decomp b) /. k = <*b19,b29*> and
A16: b = b19 + b29 by PRE_POLY:68;
( b19 = b1 & b29 = b2 ) by A9, A15, FINSEQ_1:77;
hence x9 in { H₁(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } by A14, A13, A16; :: thesis: verum

end;

A17: Support p is finite by Def5;
{ H₁(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } is finite from FRAENKEL:sch 22(A17, A1);
hence p *' q is finite-Support by A2; :: thesis: verum