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

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