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