let m, n be non zero Element of NAT ; :: thesis: ( not m,n are_coprime implies Moebius (m * n) = 0 )
assume not m,n are_coprime ; :: thesis: Moebius (m * n) = 0
then consider p being prime Nat such that
A1: ( p divides m & p divides n ) by PYTHTRIP:def 2;
reconsider p = p as prime Element of NAT by ORDINAL1:def 12;
p * p divides m * n by A1, NAT_3:1;
then p |^ 2 divides m * n by WSIERP_1:1;
then m * n is square-containing ;
hence Moebius (m * n) = 0 by Def3; :: thesis: verum