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