let X be set ; :: thesis: for p, q being bag of X st support p = {} & support q = {} holds
p = q
let p, q be bag of X; :: thesis: ( support p = {} & support q = {} implies p = q )
assume that
A1: support p = {} and
A2: support q = {} ; :: thesis: p = q
A3: {} = (dom q) /\ {}
.= dom (q | (support q)) by A2 ;
A4: dom (p | (support p)) = (dom p) /\ (support p) by RELAT_1:61
.= {} by A1 ;
then for x being object st x in dom (p | (support p)) holds
(p | (support p)) . x = (q | (support q)) . x ;
hence p = q by A4, A3, Th3, FUNCT_1:2; :: thesis: verum