let f be natural-valued finite-support Function; :: thesis: for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
F is positive-yielding
set b = (EmptyBag SetPrimes) +* f;
set C = canFS (support ((EmptyBag SetPrimes) +* f));
let F be real-valued FinSequence; :: thesis: ( F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) implies F is positive-yielding )
assume A1: F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) ; :: thesis: F is positive-yielding
A2: dom (((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f)))) = dom (canFS (support ((EmptyBag SetPrimes) +* f))) by Th13;
A3: rng (canFS (support ((EmptyBag SetPrimes) +* f))) = support ((EmptyBag SetPrimes) +* f) by FUNCT_2:def 3;
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 F or not r <= 0 )
assume r in rng F ; :: thesis: not r <= 0
then consider x being object such that
A4: x in dom F and
A5: F . x = r by FUNCT_1:def 3;
(canFS (support ((EmptyBag SetPrimes) +* f))) . x in rng (canFS (support ((EmptyBag SetPrimes) +* f))) by A1, A2, A4, FUNCT_1:def 3;
then ((EmptyBag SetPrimes) +* f) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . x) <> 0 by A3, PRE_POLY:def 7;
hence 0 < r by A1, A4, A5, FUNCT_1:12; :: thesis: verum