let F be Field; :: thesis: for E being FieldExtension of F
for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( a is_a_root_of p,E iff multiplicity (p,a) >= 1 )
let E be FieldExtension of F; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F)
for a being Element of E holds
( a is_a_root_of p,E iff multiplicity (p,a) >= 1 )
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: for a being Element of E holds
( a is_a_root_of p,E iff multiplicity (p,a) >= 1 )
let a be Element of E; :: thesis: ( a is_a_root_of p,E iff multiplicity (p,a) >= 1 )
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring E) ;
p <> 0_. F ;
then q <> 0_. E by FIELD_4:12;
then reconsider q = q as non zero Element of the carrier of (Polynom-Ring E) by UPROOTS:def 5;

A: now :: thesis: ( multiplicity (p,a) >= 1 implies a is_a_root_of p,E )

assume multiplicity (p,a) >= 1 ; :: thesis: a is_a_root_of p,E
then B: multiplicity (q,a) >= 1 by FIELD_14:def 6;
(X- a) `^ (multiplicity (q,a)) divides q by FIELD_14:67;
then (X- a) `^ 1 divides q by B, FIELD_14:40;
then X- a divides q by POLYNOM5:16;
then 0. E = eval (q,a) by RING_5:11
.= Ext_eval (p,a) by FIELD_4:26 ;
hence a is_a_root_of p,E by FIELD_4:def 2; :: thesis: verum

end;

now :: thesis: ( a is_a_root_of p,E implies multiplicity (p,a) >= 1 )

assume a is_a_root_of p,E ; :: thesis: multiplicity (p,a) >= 1
then 0. E = Ext_eval (p,a) by FIELD_4:def 2
.= eval (q,a) by FIELD_4:26 ;
then X- a divides q by RING_5:11;
then (X- a) `^ 1 divides q by POLYNOM5:16;
then multiplicity (q,a) >= 1 by mulzero1;
hence multiplicity (p,a) >= 1 by FIELD_14:def 6; :: thesis: verum

end;

hence ( a is_a_root_of p,E iff multiplicity (p,a) >= 1 ) by A; :: thesis: verum