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 TH11A, A0
.= (v1 (#) w1) . n by VALUED_1:5 ; :: thesis: verum

end;

hence v * w = v1 (#) w1 ; :: thesis: verum