deffunc H1( Element of Bags n, Element of Bags n) -> ManySortedSet of n = 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 p is finite
by Def10;
A2:
Support q is finite
by Def10;
A3:
{ 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(A1, 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 x' be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x' in Support (p *' q) or x' in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } )
assume A4:
x' in Support (p *' q)
;
:: thesis: x' in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }
then reconsider b =
x' as
Element of
Bags n ;
A5:
(p *' q) . b <> 0. L
by A4, Def9;
consider s being
FinSequence of the
carrier of
L such that A6:
(p *' q) . b = Sum s
and A7:
len s = len (decomp b)
and A8:
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 Def26;
consider k being
Nat such that A9:
k in dom s
and A10:
s /. k <> 0. L
by A5, A6, MATRLIN:15;
consider b1,
b2 being
bag of
n such that A11:
(decomp b) /. k = <*b1,b2*>
and A12:
s /. k = (p . b1) * (q . b2)
by A8, A9;
A13:
(
b1 in Bags n &
b2 in Bags n )
by Def14;
(
p . b1 <> 0. L &
q . b2 <> 0. L )
by A10, A12, VECTSP_1:36, VECTSP_1:39;
then A14:
(
b1 in Support p &
b2 in Support q )
by A13, Def9;
k in dom (decomp b)
by A7, A9, FINSEQ_3:31;
then consider b1',
b2' being
bag of
n such that A15:
(decomp b) /. k = <*b1',b2'*>
and A16:
b = b1' + b2'
by Th72;
(
b1' = b1 &
b2' = b2 )
by A11, A15, GROUP_7:2;
hence
x' in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }
by A14, A16;
:: thesis: verum
end;
then
Support (p *' q) is finite
by A3;
hence
p *' q is finite-Support
by Def10; :: thesis: verum