:: deftheorem defines denomi-seq E_TRANS1:def 4 :
for f being Element of the carrier of (Polynom-Ring F_Rat) holds denomi-seq f = canFS (denomi-set f);