let I be set ; :: thesis: for a, b being bag of I st a <> EmptyBag I holds
a + b <> EmptyBag I
let a, b be bag of I; :: thesis: ( a <> EmptyBag I implies a + b <> EmptyBag I )
given i being object such that A1: ( i in I & a . i <> (EmptyBag I) . i ) ; :: according to PBOOLE:def 10 :: thesis: a + b <> EmptyBag I
take i ; :: according to PBOOLE:def 10 :: thesis: ( i in I & not (a + b) . i = (EmptyBag I) . i )
thus i in I by A1; :: thesis: not (a + b) . i = (EmptyBag I) . i
(EmptyBag I) . i = 0 by A1, FUNCOP_1:7;
then (a . i) + (b . i) <> (EmptyBag I) . i by A1;
hence not (a + b) . i = (EmptyBag I) . i by PRE_POLY:def 5; :: thesis: verum