let f be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: for i being Nat st i in dom (denomi-seq f) holds
( (denomi-seq f) . i in NAT & (denomi-seq f) . i <> 0 )
let i be Nat; :: thesis: ( i in dom (denomi-seq f) implies ( (denomi-seq f) . i in NAT & (denomi-seq f) . i <> 0 ) )
assume A1: i in dom (denomi-seq f) ; :: thesis: ( (denomi-seq f) . i in NAT & (denomi-seq f) . i <> 0 )
reconsider TfS = denomi-set f as non empty finite Subset of NAT ;
rng (canFS TfS) = TRANQN .: (rng f) by FUNCT_2:def 3;
then (canFS TfS) . i in TRANQN .: (rng f) by A1, FUNCT_1:3;
then consider x being object such that
A2: ( x in dom TRANQN & x in rng f & (canFS TfS) . i = TRANQN . x ) by FUNCT_1:def 6;
reconsider r = x as Rational by A2;
TRANQN . x = denominator r by DIOPHAN2:def 4;
hence ( (denomi-seq f) . i in NAT & (denomi-seq f) . i <> 0 ) by A2, ORDINAL1:def 12; :: thesis: verum