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

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: h . n = (a (#) v1) . n
thus h . n = a * (v1 . n) by TH12, A0
.= (a (#) v1) . n by VALUED_1:6 ; :: thesis: verum

end;

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