let f, g be Point of R_Algebra_of_Big_Oh_poly; :: thesis: for f1, g1 being Point of (RAlgebra NAT) st f = f1 & g = g1 holds
f + g = f1 + g1
let f1, g1 be Point of (RAlgebra NAT); :: thesis: ( f = f1 & g = g1 implies f + g = f1 + g1 )
assume A1: ( f = f1 & g = g1 ) ; :: thesis: f + g = f1 + g1
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 f + g = ((RealFuncAdd NAT) || Big_Oh_poly) . [f,g] by defAlgebra
.= f1 + g1 by A1, A3, FUNCT_1:49 ; :: thesis: verum