let a be Prime; for b being bag of SetPrimes st b is prime-factorization-like & a in support b holds
( a divides Product b & ex n being Nat st a |^ n divides Product b )
let b be bag of SetPrimes ; ( b is prime-factorization-like & a in support b implies ( a divides Product b & ex n being Nat st a |^ n divides Product b ) )
assume that
A1:
b is prime-factorization-like
and
A2:
a in support b
; ( a divides Product b & ex n being Nat st a |^ n divides Product b )
consider n being Nat such that
A3:
0 < n
and
A4:
b . a = a |^ n
by A1, A2;
A5:
a divides b . a
by A3, A4, NAT_3:3;
A6:
rng b c= NAT
by VALUED_0:def 6;
a in rng (canFS (support b))
by A2, FUNCT_2:def 3;
then consider d being object such that
A7:
d in dom (canFS (support b))
and
A8:
a = (canFS (support b)) . d
by FUNCT_1:def 3;
consider f being FinSequence of COMPLEX such that
A9:
Product b = Product f
and
A10:
f = b * (canFS (support b))
by NAT_3:def 5;
rng f c= rng b
by A10, RELAT_1:26;
then
rng f c= NAT
by A6;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
A11:
rng (canFS (support b)) = support b
by FUNCT_2:def 3;
support b c= dom b
by PRE_POLY:37;
then A12:
dom f = dom (canFS (support b))
by A10, A11, RELAT_1:27;
then
b . a = (b * (canFS (support b))) . d
by A10, A7, A8, FUNCT_1:12;
then
b . a in rng f
by A10, A12, A7, FUNCT_1:3;
then
a |^ n divides Product f
by A4, NAT_3:7;
hence
( a divides Product b & ex n being Nat st a |^ n divides Product b )
by A9, A4, A5, NAT_D:4; verum