deffunc H_{1}( 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_{1}(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;

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

consider b being Function of the carrier of L,NAT such that

A1: for x being Element of L holds b . x = H

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 ) )

then
support b = Roots p
by TARSKI:2;( ( 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 ) )

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;hereby :: thesis: ( x in Roots p implies x in support b )

assume A6:
x in Roots p
; :: thesis: x in support bassume 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_{1}(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;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

then xx is_a_root_of p by A5, Th49;

hence x in Roots p by POLYNOM5:def 10; :: thesis: verum

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

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