let n be non zero Nat; :: thesis: Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) divides n
set E = Euler n;
set b0 = ppf n;
set F1 = Euler_factorization_1 n;
set b1 = (EmptyBag SetPrimes) +* (Euler_factorization_1 n);
consider f0 being FinSequence of COMPLEX such that
A1: Product (ppf n) = Product f0 and
A2: f0 = (ppf n) * (canFS (support (ppf n))) by NAT_3:def 5;
consider f1 being FinSequence of COMPLEX such that
A3: Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) = Product f1 and
A4: f1 = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) * (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) by NAT_3:def 5;
A5: support (ppf n) = support (pfexp n) by NAT_3:def 9;
A6: support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) = support (Euler_factorization_1 n) by Th12;
A7: support (Euler_factorization_1 n) = dom (Euler_factorization_1 n) by Th28;
A8: dom (Euler_factorization_1 n) = support (ppf n) by Def2;
A9: dom f0 = dom (canFS (support (ppf n))) by A2, Th13;
A10: rng (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) c= support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) by FINSEQ_1:def 4;
A11: dom f1 = dom (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) by A4, Th13;
then A12: len f0 = len f1 by A6, A7, A8, A9, FINSEQ_3:29;
rng f0 c= NAT by A2, ORDINAL1:def 12;
then reconsider f0 = f0 as FinSequence of NAT by FINSEQ_1:def 4;
rng f1 c= NAT by A4, ORDINAL1:def 12;
then reconsider f1 = f1 as FinSequence of NAT by FINSEQ_1:def 4;
for x being Nat st 1 <= x & x <= len f1 holds
f1 . x divides f0 . x

proof

let x be Nat; :: thesis: ( 1 <= x & x <= len f1 implies f1 . x divides f0 . x )
assume that
A13: 1 <= x and
A14: x <= len f1 ; :: thesis: f1 . x divides f0 . x
set p = (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x;
A15: x in dom f1 by A13, A14, FINSEQ_3:25;
dom (((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) * (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n))))) c= dom (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) by RELAT_1:25;
then A16: (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x in rng (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) by A4, A15, FUNCT_1:def 3;
then consider c being non zero Nat such that
A17: c = ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) |-count n and
A18: (Euler_factorization_1 n) . ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) = ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) |^ (c - 1) by A6, A7, A10, Def2;
A19: f1 . x = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) . ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) by A4, A15, FUNCT_1:12
.= ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) |^ (c - 1) by A6, A7, A10, A16, A18, FUNCT_4:13 ;
A20: f0 . x = (ppf n) . ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) by A2, A6, A7, A8, A9, A11, A13, A14, FINSEQ_3:25, FUNCT_1:12
.= ((canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)))) . x) |^ c by A5, A6, A7, A8, A10, A16, A17, NAT_3:def 9 ;
c - 1 <= c - 0 by XREAL_1:7;
hence f1 . x divides f0 . x by A19, A20, NEWTON:89; :: thesis: verum

end;

then Product f1 divides Product f0 by A12, Th32;
hence Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) divides n by A1, A3, NAT_3:61; :: thesis: verum