let R be domRing; :: thesis: for a, b being Element of R st b <> a holds
multiplicity ((rpoly (1,a)),b) = 0
let a, b be Element of R; :: thesis: ( b <> a implies multiplicity ((rpoly (1,a)),b) = 0 )
set p = rpoly (1,a);
assume a <> b ; :: thesis: multiplicity ((rpoly (1,a)),b) = 0
then not rpoly (1,b) divides rpoly (1,a) by div100;
hence multiplicity ((rpoly (1,a)),b) = 0 by multipp0; :: thesis: verum