let f, g be ext-real-valued FinSequence; :: thesis: ( f ^ g is positive-yielding implies ( f is positive-yielding & g is positive-yielding ) )
assume A1: f ^ g is positive-yielding ; :: thesis: ( f is positive-yielding & g is positive-yielding )
thus f is positive-yielding :: thesis: g is positive-yielding

proof

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
A2: x in dom f and
A3: f . x = r by FUNCT_1:def 3;
A4: f . x in rng f by A2, FUNCT_1:def 3;
rng f c= rng (f ^ g) by FINSEQ_1:29;
hence not r <= 0 by A1, A3, A4, PARTFUN3:def 1; :: thesis: verum

end;

thus g is positive-yielding :: thesis: verum

proof

let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 g or not r <= 0 )
assume r in rng g ; :: thesis: not r <= 0
then consider x being object such that
A5: x in dom g and
A6: g . x = r by FUNCT_1:def 3;
A7: g . x in rng g by A5, FUNCT_1:def 3;
rng g c= rng (f ^ g) by FINSEQ_1:30;
hence not r <= 0 by A1, A6, A7, PARTFUN3:def 1; :: thesis: verum

end;