let a be Prime; :: thesis: for b being bag of st b is prime-factorization-like & a divides Product b holds
a in support b
let b be bag of ; :: thesis: ( b is prime-factorization-like & a divides Product b implies a in support b )
assume A1: ( b is prime-factorization-like & a divides Product b ) ; :: thesis: a in support b

per cases ( Product b = 1 or Product b <> 1 ) ;

suppose A2: Product b = 1 ; :: thesis: a in support b

a <> 1 by INT_2:def 5;
hence a in support b by A1, A2, WSIERP_1:20; :: thesis: verum

end;

suppose A4: Product b <> 1 ; :: thesis: a in support b

consider f being FinSequence of COMPLEX such that
A5: ( Product b = Product f & f = b * (canFS (support b)) ) by NAT_3:def 5;
A6: rng b c= NAT by VALUED_0:def 6;
rng f c= rng b by A5, RELAT_1:45;
then rng f c= NAT by A6, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
( b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) ) by A1, A4, A5;
hence a in support b by Th6; :: thesis: verum

end;

end;