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

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