let f be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: for i being Nat holds
( denominator (f . i) in denomi-set f & ex z being Integer st z * (denominator (f . i)) = Product (denomi-seq f) )
let i be Nat; :: thesis: ( denominator (f . i) in denomi-set f & ex z being Integer st z * (denominator (f . i)) = Product (denomi-seq f) )
dom f = NAT by FUNCT_2:def 1;
then A2: f . i in rng f by FUNCT_1:3, ORDINAL1:def 12;
f . i in RAT by RAT_1:def 2;
then f . i in dom TRANQN by FUNCT_2:def 1;
then A4: TRANQN . (f . i) in TRANQN .: (rng f) by A2, FUNCT_1:def 6;
then denominator (f . i) in denomi-set f by DIOPHAN2:def 4;
then denominator (f . i) in rng (denomi-seq f) by FUNCT_2:def 3;
then consider j being object such that
A6: ( j in dom (denomi-seq f) & (denomi-seq f) . j = denominator (f . i) ) by FUNCT_1:def 3;
ex z being Integer st z * ((denomi-seq f) . j) = Product (denomi-seq f) by A6, INT_6:10;
hence ( denominator (f . i) in denomi-set f & ex z being Integer st z * (denominator (f . i)) = Product (denomi-seq f) ) by DIOPHAN2:def 4, A4, A6; :: thesis: verum