let f be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: not Product (denomi-seq f) is zero
reconsider denomf = denomi-seq f as real-valued FinSequence ;
A1: for n being Nat st n in dom denomf holds
denomf . n > 0

proof

let n be Nat; :: thesis: ( n in dom denomf implies denomf . n > 0 )
assume n in dom denomf ; :: thesis: denomf . n > 0
then ( (denomi-seq f) . n in NAT & (denomi-seq f) . n <> 0 ) by Lm10;
hence denomf . n > 0 ; :: thesis: verum

end;

reconsider denomf = denomf as real-valued positive-yielding FinSequence by A1, RVSUM_3:def 1;
not Product denomf is zero ;
hence not Product (denomi-seq f) is zero ; :: thesis: verum