let p be Prime; :: thesis: for n being Element of NAT st 1 <= n & not n * p is square-containing holds
Moebius (n * p) = - (Moebius n)
let a be Element of NAT ; :: thesis: ( 1 <= a & not a * p is square-containing implies Moebius (a * p) = - (Moebius a) )
assume A1: ( 1 <= a & not a * p is square-containing ) ; :: thesis: Moebius (a * p) = - (Moebius a)
then A2: a <> 0 ;
A3: p in NAT by ORDINAL1:def 13;
a,p are_relative_prime

proof

assume not a,p are_relative_prime ; :: thesis: contradiction
then consider q being prime Nat such that
A4: ( q divides a & q divides p ) by PYTHTRIP:def 2;
( q = 1 or q = p ) by A4, INT_2:def 5;
then p * p divides a * p by A3, A4, INT_2:def 5, PYTHTRIP:7;
then p |^ 2 divides a * p by WSIERP_1:2;
hence contradiction by A1, Def1; :: thesis: verum

end;

then Moebius (a * p) = (Moebius a) * (Moebius p) by A2, A3, Th35
.= (Moebius a) * (- 1) by Th34 ;
hence Moebius (a * p) = - (Moebius a) ; :: thesis: verum