let v, w be VECTOR of R_Algebra_of_Big_Oh_poly; :: thesis: for v1, w1 being Function of NAT,REAL st v = v1 & w1 = w holds
v + w = v1 + w1
let v1, w1 be Function of NAT,REAL; :: thesis: ( v = v1 & w1 = w implies v + w = v1 + w1 )
assume A0: ( v = v1 & w1 = w ) ; :: thesis: v + w = v1 + w1
v + w in the carrier of R_Algebra_of_Big_Oh_poly ;
then v + w in Big_Oh_poly by defAlgebra;
then reconsider h = v + w as Function of NAT,REAL by DefX1;
h = v1 + w1

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: h . n = (v1 + w1) . n
thus h . n = (v1 . n) + (w1 . n) by A0, TH11
.= (v1 + w1) . n by VALUED_1:1 ; :: thesis: verum

end;

hence v + w = v1 + w1 ; :: thesis: verum