Ext_eval (p,(KrRootP p)) = 0. F by FIELD_5:17
.= 0. (embField (canHomP p)) by FIELD_2:def 7 ;
hence KrRootP p is F -algebraic by FIELD_6:43; :: thesis: verum