let p be Prime; :: thesis: for f being positive-yielding bag of Seg p st f = p |-> p holds
Product f = p |^ p
let f be positive-yielding bag of Seg p; :: thesis: ( f = p |-> p implies Product f = p |^ p )
assume A0: f = p |-> p ; :: thesis: Product f = p |^ p
consider g being FinSequence of COMPLEX such that
A1: ( Product f = Product g & g = f * (canFS (support f)) ) by NAT_3:def 5;
g = f by ThCon, A0, A1;
hence Product f = p |^ p by A1, A0, NEWTON:def 1; :: thesis: verum