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 pt holds

pt . q = f . q

let q be Nat; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: verum

pt . q = f . q

let q be Nat; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: verum