let L be Field; :: thesis: for a, x being Element of L
for b being non zero Element of L holds
( x is_a_root_of <%a,b%> iff x = - (a / b) )
let a, x be Element of L; :: thesis: for b being non zero Element of L holds
( x is_a_root_of <%a,b%> iff x = - (a / b) )
let b be non zero Element of L; :: thesis: ( x is_a_root_of <%a,b%> iff x = - (a / b) )
set p = <%a,b%>;

hereby :: thesis: ( x = - (a / b) implies x is_a_root_of <%a,b%> )

assume A1: x is_a_root_of <%a,b%> ; :: thesis: x = - (a / b)
b * (/ b) = (/ b) * b ;
then A2: (b * x) / b = x by Th4;
a + (b * x) = 0. L by A1, POLYNOM5:44;
then b * x = - a by RLVECT_1:6;
hence x = - (a / b) by A2, VECTSP_1:9; :: thesis: verum

end;

assume x = - (a / b) ; :: thesis: x is_a_root_of <%a,b%>
hence eval (<%a,b%>,x) = 0. L by Th8; :: according to POLYNOM5:def 7 :: thesis: verum