let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F)
for a being non zero Element of F holds MonicDivisors p = MonicDivisors (a * p)
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: for a being non zero Element of F holds MonicDivisors p = MonicDivisors (a * p)
let a be non zero Element of F; :: thesis: MonicDivisors p = MonicDivisors (a * p)

A: now :: thesis: for o being object st o in MonicDivisors p holds
o in MonicDivisors (a * p)

let o be object ; :: thesis: ( o in MonicDivisors p implies o in MonicDivisors (a * p) )
assume o in MonicDivisors p ; :: thesis: o in MonicDivisors (a * p)
then consider q being monic Element of the carrier of (Polynom-Ring F) such that
B: ( o = q & q divides p ) ;
q divides a * p by B, RING_5:15;
hence o in MonicDivisors (a * p) by B; :: thesis: verum

end;

now :: thesis: for o being object st o in MonicDivisors (a * p) holds
o in MonicDivisors p

let o be object ; :: thesis: ( o in MonicDivisors (a * p) implies o in MonicDivisors p )
assume o in MonicDivisors (a * p) ; :: thesis: o in MonicDivisors p
then consider q being monic Element of the carrier of (Polynom-Ring F) such that
B: ( o = q & q divides a * p ) ;
q divides p by B, RING_5:15;
hence o in MonicDivisors p by B; :: thesis: verum

end;

hence MonicDivisors p = MonicDivisors (a * p) by A, TARSKI:2; :: thesis: verum