let F be Field; :: thesis: for p being Ppoly of F holds
( p is Ppoly of F,(Roots p) iff for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 )
let p be Ppoly of F; :: thesis: ( p is Ppoly of F,(Roots p) iff for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 )
set P = Roots p;

A: now :: thesis: ( p is Ppoly of F,(Roots p) implies for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 )

assume A: p is Ppoly of F,(Roots p) ; :: thesis: for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1
B: Bag (Roots p) = ((Roots p),1) -bag by RING_5:def 1;
thus for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 :: thesis: verum

proof

let a be Element of F; :: thesis: ( a is_a_root_of p implies multiplicity (p,a) = 1 )
assume a is_a_root_of p ; :: thesis: multiplicity (p,a) = 1
then a in Roots p by POLYNOM5:def 10;
then (((Roots p),1) -bag) . a = 1 by UPROOTS:7;
hence multiplicity (p,a) = 1 by B, A, RING_5:def 5; :: thesis: verum

end;

end;

now :: thesis: ( ( for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 ) implies p is Ppoly of F,(Roots p) )

assume A: for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 ; :: thesis: p is Ppoly of F,(Roots p)
B: p is Ppoly of F, BRoots p by RING_5:59;
BRoots p = ((Roots p),1) -bag

proof

now :: thesis: for o being object st o in the carrier of F holds
(BRoots p) . o = (((Roots p),1) -bag) . o

let o be object ; :: thesis: ( o in the carrier of F implies (BRoots p) . b₁ = (((Roots p),1) -bag) . b₁ )
assume o in the carrier of F ; :: thesis: (BRoots p) . b₁ = (((Roots p),1) -bag) . b₁
then reconsider a = o as Element of F ;

per cases ( not a is_a_root_of p or a is_a_root_of p ) ;

suppose B0: not a is_a_root_of p ; :: thesis: (BRoots p) . b₁ = (((Roots p),1) -bag) . b₁

then B1: multiplicity (p,a) = 0 by NAT_1:14, UPROOTS:52;
B2: not a in Roots p by B0, POLYNOM5:def 10;
thus (BRoots p) . o = 0 by B1, UPROOTS:def 9
.= (((Roots p),1) -bag) . o by B2, UPROOTS:6 ; :: thesis: verum

end;

suppose B0: a is_a_root_of p ; :: thesis: (BRoots p) . b₁ = (((Roots p),1) -bag) . b₁

then B1: multiplicity (p,a) = 1 by A;
B2: a in Roots p by B0, POLYNOM5:def 10;
thus (BRoots p) . o = 1 by B1, UPROOTS:def 9
.= (((Roots p),1) -bag) . o by B2, UPROOTS:7 ; :: thesis: verum

end;

end;

end;

hence BRoots p = ((Roots p),1) -bag by PBOOLE:3; :: thesis: verum

end;

hence p is Ppoly of F,(Roots p) by B, RING_5:def 1; :: thesis: verum

end;

hence ( p is Ppoly of F,(Roots p) iff for a being Element of F st a is_a_root_of p holds
multiplicity (p,a) = 1 ) by A; :: thesis: verum