let a be Prime; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ;
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; :: thesis: verum