let ps, pt, f be bag of SetPrimes ; for q being Nat st support ps misses support pt & f = ps + pt & q in support pt holds
pt . q = f . q
let q be Nat; ( support ps misses support pt & f = ps + pt & q in support pt implies pt . q = f . q )
assume A1:
( support ps misses support pt & f = ps + pt & q in support pt )
; pt . q = f . q
then
(support ps) /\ (support pt) = {}
by XBOOLE_0:def 7;
then A2:
not q in support ps
by A1, XBOOLE_0:def 4;
thus f . q =
(ps . q) + (pt . q)
by A1, PRE_POLY:def 5
.=
0 + (pt . q)
by A2, PRE_POLY:def 7
.=
pt . q
; verum