let a be Prime; :: thesis: for b being bag of st b is prime-factorization-like & a in support b holds
( a divides Product b & ex n being natural number st a |^ n divides Product b )
let b be bag of ; :: thesis: ( b is prime-factorization-like & a in support b implies ( a divides Product b & ex n being natural number st a |^ n divides Product b ) )
assume A1: ( b is prime-factorization-like & a in support b ) ; :: thesis: ( a divides Product b & ex n being natural number st a |^ n divides Product b )
consider f being FinSequence of COMPLEX such that
A2: ( Product b = Product f & f = b * (canFS (support b)) ) by NAT_3:def 5;
A3: rng b c= NAT by VALUED_0:def 6;
rng f c= rng b by A2, RELAT_1:45;
then rng f c= NAT by A3, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
A4: support b c= dom b by POLYNOM1:41;
rng (canFS (support b)) = support b by FUNCT_2:def 3;
then A5: dom f = dom (canFS (support b)) by A2, A4, RELAT_1:46;
A6: a in rng (canFS (support b)) by A1, FUNCT_2:def 3;
consider n being natural number such that
A7: ( 0 < n & b . a = a |^ n ) by A1, Def1;
consider d being set such that
A8: ( d in dom (canFS (support b)) & a = (canFS (support b)) . d ) by A6, FUNCT_1:def 5;
b . a = (b * (canFS (support b))) . d by A2, A5, A8, FUNCT_1:22;
then b . a in rng f by A2, A5, A8, FUNCT_1:12;
then A9: a |^ n divides Product f by A7, NAT_3:7;
a divides b . a by A7, NAT_3:3;
hence ( a divides Product b & ex n being natural number st a |^ n divides Product b ) by A2, A7, A9, NAT_D:4; :: thesis: verum