let f be FinSequence of NAT ; :: thesis: for b being bag of SetPrimes
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 SetPrimes ; :: 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 that
A1: b is prime-factorization-like and
A2: Product b <> 1 and
A3: a divides Product b and
A4: Product b = Product f and
A5: f = b * (canFS (support b)) ; :: thesis: a in support b
len f is Element of NAT ;
hence a in support b by A1, A2, A3, A4, A5, Lm6; :: thesis: verum