let f be Point of R_Algebra_of_Big_Oh_poly; :: thesis: for f1 being Point of (RAlgebra NAT)
for a being Element of REAL st f = f1 holds
a * f = a * f1
let f1 be Point of (RAlgebra NAT); :: thesis: for a being Element of REAL st f = f1 holds
a * f = a * f1
let a be Element of REAL ; :: thesis: ( f = f1 implies a * f = a * f1 )
assume A1: f = f1 ; :: thesis: a * f = a * f1
set X = Big_Oh_poly ;
set S = R_Algebra_of_Big_Oh_poly ;
A3: the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;
thus a * f = ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) . [a,f] by defAlgebra
.= a * f1 by A1, A3, FUNCT_1:49 ; :: thesis: verum