let s, t be non zero Nat; :: thesis: ( s,t are_coprime implies (EmptyBag SetPrimes) +* (Euler_factorization (s * t)) = ((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t)) )
assume A1: s,t are_coprime ; :: thesis: (EmptyBag SetPrimes) +* (Euler_factorization (s * t)) = ((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t))
set n = s * t;
set N = Euler_factorization (s * t);
set S = Euler_factorization s;
set T = Euler_factorization t;
for x being object st x in SetPrimes holds
((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x)

proof

let x be object ; :: thesis: ( x in SetPrimes implies ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x) )
assume x in SetPrimes ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x)
then reconsider p = x as Prime by NEWTON:def 6;
A2: p |-count (s * t) = (p |-count s) + (p |-count t) by NAT_3:28;
A3: dom (Euler_factorization s) = support (ppf s) by Def1;
A4: dom (Euler_factorization t) = support (ppf t) by Def1;
A5: dom (Euler_factorization (s * t)) = support (ppf (s * t)) by Def1;
ppf (s * t) = (ppf s) + (ppf t) by A1, NAT_3:58;
then A6: dom (Euler_factorization (s * t)) = (dom (Euler_factorization s)) \/ (dom (Euler_factorization t)) by A3, A4, A5, PRE_POLY:38;

per cases ( x in dom (Euler_factorization s) or x in dom (Euler_factorization t) or ( not x in dom (Euler_factorization s) & not x in dom (Euler_factorization t) ) ) ;

suppose A7: x in dom (Euler_factorization s) ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x)

then A8: not x in dom (Euler_factorization t) by A1, Th24, XBOOLE_0:3;
then A9: ((EmptyBag SetPrimes) +* (Euler_factorization t)) . x = (EmptyBag SetPrimes) . x by FUNCT_4:11;
A10: p |-count t = 0 by A4, A8, MOEBIUS1:15;
A11: x in dom (Euler_factorization (s * t)) by A6, A7, XBOOLE_0:def 3;
then A12: ex c being non zero Nat st
( c = p |-count (s * t) & (Euler_factorization (s * t)) . p = (p |^ c) - (p |^ (c - 1)) ) by Def1;
ex c being non zero Nat st
( c = p |-count s & (Euler_factorization s) . p = (p |^ c) - (p |^ (c - 1)) ) by A7, Def1;
hence (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x) = (Euler_factorization (s * t)) . x by A2, A7, A9, A10, A12, FUNCT_4:13
.= ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x by A11, FUNCT_4:13 ;
:: thesis: verum

end;

suppose A13: x in dom (Euler_factorization t) ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x)

A14: not x in dom (Euler_factorization s) by A1, A13, Th24, XBOOLE_0:3;
then A15: ((EmptyBag SetPrimes) +* (Euler_factorization s)) . x = (EmptyBag SetPrimes) . x by FUNCT_4:11;
A16: p |-count s = 0 by A3, A14, MOEBIUS1:15;
A17: x in dom (Euler_factorization (s * t)) by A6, A13, XBOOLE_0:def 3;
then A18: ex c being non zero Nat st
( c = p |-count (s * t) & (Euler_factorization (s * t)) . p = (p |^ c) - (p |^ (c - 1)) ) by Def1;
ex c being non zero Nat st
( c = p |-count t & (Euler_factorization t) . p = (p |^ c) - (p |^ (c - 1)) ) by A13, Def1;
hence (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x) = (Euler_factorization (s * t)) . x by A2, A13, A15, A16, A18, FUNCT_4:13
.= ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x by A17, FUNCT_4:13 ;
:: thesis: verum

end;

suppose A19: ( not x in dom (Euler_factorization s) & not x in dom (Euler_factorization t) ) ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x)

then A20: not x in dom (Euler_factorization (s * t)) by A6, XBOOLE_0:def 3;
( ((EmptyBag SetPrimes) +* (Euler_factorization s)) . x = (EmptyBag SetPrimes) . x & ((EmptyBag SetPrimes) +* (Euler_factorization t)) . x = (EmptyBag SetPrimes) . x ) by A19, FUNCT_4:11;
hence ((EmptyBag SetPrimes) +* (Euler_factorization (s * t))) . x = (((EmptyBag SetPrimes) +* (Euler_factorization s)) . x) + (((EmptyBag SetPrimes) +* (Euler_factorization t)) . x) by A20, FUNCT_4:11; :: thesis: verum

end;

end;

end;

hence (EmptyBag SetPrimes) +* (Euler_factorization (s * t)) = ((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t)) by PRE_POLY:33; :: thesis: verum