let a be Nat; :: thesis: PrimeDivisors (a * a) = PrimeDivisors a
PrimeDivisors (a * a) = (PrimeDivisors a) \/ (PrimeDivisors a) by DivisorsMulti
.= PrimeDivisors a ;
hence PrimeDivisors (a * a) = PrimeDivisors a ; :: thesis: verum