let a, b be non zero Nat; :: thesis: ( a,b are_coprime implies Moebius (a * b) = (Moebius a) * (Moebius b) )
assume A1: a,b are_coprime ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

per cases ( ( a is square-free & b is square-free ) or ( a is square-free & b is square-containing ) or ( a is square-containing & b is square-free ) or ( a is square-containing & b is square-containing ) ) ;

suppose A2: ( a is square-free & b is square-free ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

A3: a * b is square-free

proof

assume a * b is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A4: p |^ 2 divides a * b ;
( p |^ 2 divides a or p |^ 2 divides b ) by A1, A4, Th11;
hence contradiction by A2; :: thesis: verum

end;

A5: Moebius a = (- 1) |^ (card (support (ppf a))) by A2, Def3;
card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by A1, NAT_3:47;
then card (support (ppf (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by NAT_3:def 9
.= (card (support (pfexp a))) + (card (support (ppf b))) by NAT_3:def 9
.= (card (support (ppf a))) + (card (support (ppf b))) by NAT_3:def 9 ;
then Moebius (a * b) = (- 1) |^ ((card (support (ppf a))) + (card (support (ppf b)))) by A3, Def3
.= ((- 1) |^ (card (support (ppf a)))) * ((- 1) |^ (card (support (ppf b)))) by NEWTON:8 ;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A2, A5, Def3; :: thesis: verum

end;

suppose A6: ( a is square-free & b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

then consider p being Prime such that
A7: p |^ 2 divides b ;
p |^ 2 divides a * b by A7, NAT_D:9;
then A8: a * b is square-containing ;
Moebius b = 0 by A6, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A8, Def3; :: thesis: verum

end;

suppose A9: ( a is square-containing & b is square-free ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

then consider p being Prime such that
A10: p |^ 2 divides a ;
p |^ 2 divides a * b by A10, NAT_D:9;
then A11: a * b is square-containing ;
Moebius a = 0 by A9, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A11, Def3; :: thesis: verum

end;

suppose A12: ( a is square-containing & b is square-containing ) ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

then consider p being Prime such that
A13: p |^ 2 divides a ;
p |^ 2 divides a * b by A13, NAT_D:9;
then A14: a * b is square-containing ;
Moebius a = 0 by A12, Def3;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A14, Def3; :: thesis: verum

end;

end;