let f be bag of SetPrimes ; :: thesis: ex g being FinSequence of NAT st
( Product f = Product g & g = f * (canFS (support f)) )
consider g being FinSequence of COMPLEX such that
A2: ( Product f = Product g & g = f * (canFS (support f)) ) by NAT_3:def 5;
rng g c= NAT by A2, VALUED_0:def 6;
then g is FinSequence of NAT by FINSEQ_1:def 4;
hence ex g being FinSequence of NAT st
( Product f = Product g & g = f * (canFS (support f)) ) by A2; :: thesis: verum