let a, b be non zero Element of NAT ; :: thesis: ( a,b are_relative_prime implies Moebius (a * b) = (Moebius a) * (Moebius b) )
assume A1: a,b are_relative_prime ; :: thesis: Moebius (a * b) = (Moebius a) * (Moebius b)

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

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

then A3: ( Moebius a = (- 1) |^ (card (support (ppf a))) & Moebius b = (- 1) |^ (card (support (ppf b))) ) by Def3;
card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by A1, NAT_3:47;
then A4: 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 ;
not a * b is square-containing

proof

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

end;

then Moebius (a * b) = (- 1) |^ ((card (support (ppf a))) + (card (support (ppf b)))) by A4, Def3
.= ((- 1) |^ (card (support (ppf a)))) * ((- 1) |^ (card (support (ppf b)))) by NEWTON:13 ;
hence Moebius (a * b) = (Moebius a) * (Moebius b) by A3; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

end;