let it1, it2 be bag of the carrier of L; :: thesis: ( support it1 = Roots p & ( for x being Element of L holds it1 . x = multiplicity p,x ) & support it2 = Roots p & ( for x being Element of L holds it2 . x = multiplicity p,x ) implies it1 = it2 )
assume that
support it1 = Roots p and
A7: for x being Element of L holds it1 . x = multiplicity p,x and
support it2 = Roots p and
A8: for x being Element of L holds it2 . x = multiplicity p,x ; :: thesis: it1 = it2

now

let x be set ; :: thesis: ( x in the carrier of L implies it1 . x = it2 . x )
assume x in the carrier of L ; :: thesis: it1 . x = it2 . x
then reconsider xx = x as Element of L ;
thus it1 . x = multiplicity p,xx by A7
.= it2 . x by A8 ; :: thesis: verum

end;

hence it1 = it2 by PBOOLE:3; :: thesis: verum