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

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 :: thesis: for x being object st x in the carrier of L holds

it1 . x = it2 . x

hence
it1 = it2
by PBOOLE:3; :: thesis: verumit1 . x = it2 . x

let x be object ; :: 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;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