let f be FinSequence of NAT ; :: thesis: for b being bag of
for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let b be bag of ; :: thesis: for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let a be Prime; :: thesis: ( b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) implies a in support b )
assume A1: ( b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) ) ; :: thesis: a in support b
len f is Element of NAT ;
hence a in support b by A1, Lm6; :: thesis: verum