now :: thesis: not KrRootP p in the carrier of F

assume KrRootP p in the carrier of F ; :: thesis: contradiction
then reconsider o = KrRootP p as Element of F ;
eval (p,o) = Ext_eval (p,(KrRootP p)) by FIELD_6:10
.= 0. F by FIELD_5:17 ;
then o is_a_root_of p ;
then p is with_roots ;
hence contradiction ; :: thesis: verum

end;

hence ( not KrRootP p is zero & not KrRootP p is F -membered ) by FIELD_7:def 5; :: thesis: verum