let p be Prime; :: thesis: for f being positive-yielding bag of Seg p holds dom f = support f
let f be positive-yielding bag of Seg p; :: thesis: dom f = support f
Y1: dom f = Seg p by PARTFUN1:def 2;
Seg p c= support f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg p or x in support f )
assume x in Seg p ; :: thesis: x in support f
then f . x in rng f by Y1, FUNCT_1:3;
hence x in support f by PRE_POLY:def 7; :: thesis: verum

end;

hence dom f = support f by Y1, XBOOLE_0:def 10; :: thesis: verum