let n be Nat; :: thesis: for f being Element of the carrier of (Polynom-Ring F_Rat) holds n * f = ((In (n,F_Rat)) | F_Rat) *' (~ f)
let f be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: n * f = ((In (n,F_Rat)) | F_Rat) *' (~ f)
n * f = (In (n,F_Rat)) * f by E_TRANS1:6;
hence n * f = ((In (n,F_Rat)) | F_Rat) *' (~ f) by FIELD_8:2; :: thesis: verum