let a be Prime; :: thesis: for b being bag of SetPrimes st b is prime-factorization-like & a divides Product b holds
a in support b
let b be bag of SetPrimes ; :: thesis: ( b is prime-factorization-like & a divides Product b implies a in support b )
assume that
A1: b is prime-factorization-like and
A2: a divides Product b ; :: thesis: a in support b
per cases ( Product b = 1 or Product b <> 1 ) ;
suppose A3: Product b = 1 ; :: thesis: a in support b
a <> 1 by INT_2:def 4;
hence a in support b by A2, A3, WSIERP_1:15; :: thesis: verum
end;
suppose A4: Product b <> 1 ; :: thesis: a in support b
A5: rng b c= NAT by VALUED_0:def 6;
consider f being FinSequence of COMPLEX such that
A6: Product b = Product f and
A7: f = b * (canFS (support b)) by NAT_3:def 5;
rng f c= rng b by A7, RELAT_1:26;
then rng f c= NAT by A5;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
Product b = Product f by A6;
hence a in support b by A1, A2, A4, A7, Th6; :: thesis: verum
end;
end;