let n be non zero Nat; :: thesis: (EmptyBag SetPrimes) +* (Euler_factorization n) = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) (#) ((EmptyBag SetPrimes) +* (Euler_factorization_2 n))
set N = Euler_factorization n;
set S = Euler_factorization_1 n;
set T = Euler_factorization_2 n;
A1: dom (Euler_factorization n) = support (ppf n) by Def1;
A2: dom (Euler_factorization_1 n) = support (ppf n) by Def2;
A3: dom (Euler_factorization_2 n) = support (ppf n) by Def3;
for x being object st x in SetPrimes holds
((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x)

proof

let x be object ; :: thesis: ( x in SetPrimes implies ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x) )
assume x in SetPrimes ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x)
then reconsider p = x as Prime by NEWTON:def 6;

per cases ( x in dom (Euler_factorization n) or not x in dom (Euler_factorization n) ) ;

suppose A4: x in dom (Euler_factorization n) ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x)

then A5: ( ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (Euler_factorization n) . x & ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x = (Euler_factorization_1 n) . x & ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x = (Euler_factorization_2 n) . x ) by A1, A2, A3, FUNCT_4:13;
consider c being non zero Nat such that
A6: ( c = p |-count n & (Euler_factorization_1 n) . p = p |^ (c - 1) ) by A1, A2, A4, Def2;
ex c being non zero Nat st
( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) ) by A4, Th18;
hence ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x) by A1, A3, A4, A5, A6, Def3; :: thesis: verum

end;

suppose not x in dom (Euler_factorization n) ; :: thesis: ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x)

then ( ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (EmptyBag SetPrimes) . x & ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x = (EmptyBag SetPrimes) . x & ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x = (EmptyBag SetPrimes) . x ) by A1, A2, A3, FUNCT_4:11;
hence ((EmptyBag SetPrimes) +* (Euler_factorization n)) . x = (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . x) * (((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) . x) ; :: thesis: verum

end;

end;

end;

hence (EmptyBag SetPrimes) +* (Euler_factorization n) = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) (#) ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) by Th4; :: thesis: verum