deffunc H₁( Element of L) -> Element of NAT = multiplicity (p,$1);
consider b being Function of the carrier of L,NAT such that
A1: for x being Element of L holds b . x = H₁(x) from FUNCT_2:sch 4();
dom b = the carrier of L by FUNCT_2:def 1;
then A2: support b c= the carrier of L by PRE_POLY:37;

A3: now :: thesis: for x being object holds
( ( x in support b implies x in Roots p ) & ( x in Roots p implies x in support b ) )

let x be object ; :: thesis: ( ( x in support b implies x in Roots p ) & ( x in Roots p implies x in support b ) )

hereby :: thesis: ( x in Roots p implies x in support b )

assume A4: x in support b ; :: thesis: x in Roots p
then reconsider xx = x as Element of L by A2;
b . x <> 0 by A4, PRE_POLY:def 7;
then A5: b . xx >= 0 + 1 by NAT_1:13;
b . x = H₁(xx) by A1;
then xx is_a_root_of p by A5, Th49;
hence x in Roots p by POLYNOM5:def 10; :: thesis: verum

end;

assume A6: x in Roots p ; :: thesis: x in support b
then reconsider xx = x as Element of L ;
xx is_a_root_of p by A6, POLYNOM5:def 10;
then multiplicity (p,xx) >= 1 by Th49;
then b . xx >= 1 by A1;
hence x in support b by PRE_POLY:def 7; :: thesis: verum

end;

then support b = Roots p by TARSKI:2;
then reconsider b = b as bag of the carrier of L by PRE_POLY:def 8;
take b ; :: thesis: ( support b = Roots p & ( for x being Element of L holds b . x = multiplicity (p,x) ) )
thus ( support b = Roots p & ( for x being Element of L holds b . x = multiplicity (p,x) ) ) by A1, A3, TARSKI:2; :: thesis: verum