let f1, f2 be FinSequence of REAL ; :: thesis: ( len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k >= 0 ) ) implies Product f1 >= Product f2 )
assume A1: ( len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k >= 0 ) ) ) ; :: thesis: Product f1 >= Product f2
for r being Real st r in rng f2 holds
r >= 0

proof

let r be Real; :: thesis: ( r in rng f2 implies r >= 0 )
assume B1: r in rng f2 ; :: thesis: r >= 0
consider k being object such that
B2: ( k in dom f2 & f2 . k = r ) by B1, FUNCT_1:def 3;
reconsider k = k as Element of NAT by B2;
thus r >= 0 by A1, B2; :: thesis: verum

end;

then reconsider f2 = f2 as nonnegative-yielding FinSequence of REAL by PARTFUN3:def 4;
for r being Real st r in rng f1 holds
r >= 0

proof

let r be Real; :: thesis: ( r in rng f1 implies r >= 0 )
assume B1: r in rng f1 ; :: thesis: r >= 0
consider k being object such that
B2: ( k in dom f1 & f1 . k = r ) by B1, FUNCT_1:def 3;
reconsider k = k as Element of NAT by B2;
dom f1 = dom f2 by A1, FINSEQ_3:29;
then ( f1 . k >= f2 . k & f2 . k >= 0 ) by A1, B2;
hence r >= 0 by B2; :: thesis: verum

end;

then reconsider f1 = f1 as nonnegative-yielding FinSequence of REAL by PARTFUN3:def 4;
( len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
f1 . k >= f2 . k ) ) by A1;
hence Product f1 >= Product f2 by N454; :: thesis: verum