let m, n be non zero Nat; :: thesis: ( m,n are_coprime implies #divs (m * n) = (#divs m) * (#divs n) )
assume AA: m,n are_coprime ; :: thesis: #divs (m * n) = (#divs m) * (#divs n)
set f = EXP 0;
set X = NatDivisors m;
D4: EXP 0 is multiplicative by NAT_5:35;
XX: ( n in NAT & m in NAT & m * n in NAT ) by ORDINAL1:def 12;
for n0 being non zero Nat holds Divs . n0 = Sum ((EXP 0) | (NatDivisors n0))

proof

let n0 be non zero Nat; :: thesis: Divs . n0 = Sum ((EXP 0) | (NatDivisors n0))
n0 in NAT by ORDINAL1:def 12;
then Divs . n0 = #divs n0 by DivsDef
.= Sum ((EXP 0) | (NatDivisors n0)) by NAT_5:def 2 ;
hence Divs . n0 = Sum ((EXP 0) | (NatDivisors n0)) ; :: thesis: verum

end;

then Divs is multiplicative by D4, NAT_5:34;
then F1: Divs . (n * m) = (Divs . n) * (Divs . m) by AA, NAT_5:def 5;
( Divs . (n * m) = #divs (m * n) & Divs . n = #divs n & Divs . m = #divs m ) by XX, DivsDef;
hence #divs (m * n) = (#divs m) * (#divs n) by F1; :: thesis: verum