let f1, f2 be FinSequence of REAL ; :: thesis: ( len f1 = len f2 & ( for k being Element of NAT st k in dom f1 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 f1 holds
( f1 . k >= f2 . k & f2 . k > 0 ) ) ) ; :: thesis: Product f1 >= Product f2
for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k > 0 )

proof

let k be Element of NAT ; :: thesis: ( k in dom f2 implies ( f1 . k >= f2 . k & f2 . k > 0 ) )
assume B1: k in dom f2 ; :: thesis: ( f1 . k >= f2 . k & f2 . k > 0 )
k in dom f1 by A1, B1, FINSEQ_3:29;
hence ( f1 . k >= f2 . k & f2 . k > 0 ) by A1; :: thesis: verum

end;

hence Product f1 >= Product f2 by A1, NAT_4:54; :: thesis: verum