deffunc H1( Element of Bags n, Element of Bags n) -> set = n + L;
set D = { H1(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= { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }
proof
let x9 be
object ;
TARSKI:def 3 ( not x9 in Support (p *' q) or x9 in { H1(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)
;
x9 in { H1(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 { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }
by A14, A13, A16;
verum
end;
A17:
Support p is finite
by Def5;
{ H1(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; verum