let L be Field; :: thesis: for a, x being Element of L
for b being non zero Element of L st x <> - (a / b) holds
multiplicity (<%a,b%>,x) = 0
let a, x be Element of L; :: thesis: for b being non zero Element of L st x <> - (a / b) holds
multiplicity (<%a,b%>,x) = 0
let b be non zero Element of L; :: thesis: ( x <> - (a / b) implies multiplicity (<%a,b%>,x) = 0 )
assume A1: x <> - (a / b) ; :: thesis: multiplicity (<%a,b%>,x) = 0
set f = <%a,b%>;
Roots <%a,b%> = {(- (a / b))} by Th10;
then not x in Roots <%a,b%> by A1, TARSKI:def 1;
then not x is_a_root_of <%a,b%> by POLYNOM5:def 10;
hence multiplicity (<%a,b%>,x) = 0 by NAT_1:14, UPROOTS:52; :: thesis: verum