let n be Ordinal; :: thesis: for a, b being bag of st b divides a holds
support b c= support a
let a, b be bag of ; :: thesis: ( b divides a implies support b c= support a )
assume A1: b divides a ; :: thesis: support b c= support a
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support b or x in support a )
assume x in support b ; :: thesis: x in support a
then b . x <> 0 by POLYNOM1:def 7;
then a . x <> 0 by A1, POLYNOM1:def 13;
hence x in support a by POLYNOM1:def 7; :: thesis: verum