let I be set ; :: thesis: for m, x, y being bag of I st x divides m & x <> y holds
m <> (m -' x) + y
let m, x, y be bag of I; :: thesis: ( x divides m & x <> y implies m <> (m -' x) + y )
assume Z0: for a being object holds x . a <= m . a ; :: according to PRE_POLY:def 11 :: thesis: ( not x <> y or m <> (m -' x) + y )
given a being object such that Z1: ( a in I & x . a <> y . a ) ; :: according to PBOOLE:def 10 :: thesis: m <> (m -' x) + y
take a ; :: according to PBOOLE:def 10 :: thesis: ( a in I & not m . a = ((m -' x) + y) . a )
thus a in I by Z1; :: thesis: not m . a = ((m -' x) + y) . a
A1: ( ((m -' x) + y) . a = ((m -' x) . a) + (y . a) & ((m -' x) . a) + (y . a) = ((m . a) -' (x . a)) + (y . a) ) by PRE_POLY:def 5, PRE_POLY:def 6;
(m . a) -' (x . a) = (m . a) - (x . a) by Z0, XREAL_1:233;
hence not m . a = ((m -' x) + y) . a by A1, Z1; :: thesis: verum