let n0, m0 be non zero Nat; :: thesis: for n1, m1 being Nat st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds
n1 * m1 in NatDivisors (n0 * m0)
let n1, m1 be Nat; :: thesis: ( n1 in NatDivisors n0 & m1 in NatDivisors m0 implies n1 * m1 in NatDivisors (n0 * m0) )
reconsider b = n0 * m0 as non zero Nat ;
assume A1: n1 in NatDivisors n0 ; :: thesis: ( not m1 in NatDivisors m0 or n1 * m1 in NatDivisors (n0 * m0) )
then A2: 0 < n1 ;
A3: n1 divides n0 by A1, MOEBIUS1:39;
assume A4: m1 in NatDivisors m0 ; :: thesis: n1 * m1 in NatDivisors (n0 * m0)
then A5: 0 < m1 ;
then reconsider a = n1 * m1 as non zero Nat by A2;
A6: m1 divides m0 by A4, MOEBIUS1:39;
for p being Element of NAT st p is prime holds
p |-count a <= p |-count b

proof

reconsider n19 = n1, m19 = m1 as non zero Nat by A1, A4;
let p be Element of NAT ; :: thesis: ( p is prime implies p |-count a <= p |-count b )
assume p is prime ; :: thesis: p |-count a <= p |-count b
then reconsider p9 = p as Prime ;
A8: ( p9 |-count (n19 * m19) = (p9 |-count n19) + (p9 |-count m19) & p9 |-count (n0 * m0) = (p9 |-count n0) + (p9 |-count m0) ) by NAT_3:28;
( p9 |-count n19 <= p9 |-count n0 & p9 |-count m19 <= p9 |-count m0 ) by A3, A6, NAT_3:30;
hence p |-count a <= p |-count b by A8, XREAL_1:7; :: thesis: verum

end;

then ex c being Element of NAT st n0 * m0 = (n1 * m1) * c by NAT_4:20;
then n1 * m1 divides n0 * m0 by NAT_D:def 3;
hence n1 * m1 in NatDivisors (n0 * m0) by A2, A5; :: thesis: verum