let f, h be VECTOR of R_Algebra_of_Big_Oh_poly; :: thesis: for f9, h9 being Function of NAT,REAL st f9 = f & h9 = h holds
for a being Real holds
( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) )
let f9, h9 be Function of NAT,REAL; :: thesis: ( f9 = f & h9 = h implies for a being Real holds
( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) ) )
assume A1: ( f9 = f & h9 = h ) ; :: thesis: for a being Real holds
( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) )
let a be Real; :: thesis: ( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) )
A0: a is Element of REAL by XREAL_0:def 1;
reconsider f1 = f, h1 = h as VECTOR of (RAlgebra NAT) by LM12;

A3: now :: thesis: ( h = a * f implies for x being Nat holds h9 . x = a * (f9 . x) )

assume A4: h = a * f ; :: thesis: for x being Nat holds h9 . x = a * (f9 . x)
let x be Nat; :: thesis: h9 . x = a * (f9 . x)
LXN: x in NAT by ORDINAL1:def 12;
h1 = a * f1 by A4, LM17, A0;
hence h9 . x = a * (f9 . x) by A1, FUNCSDOM:4, LXN; :: thesis: verum

end;

now :: thesis: ( ( for x being Element of NAT holds h9 . x = a * (f9 . x) ) implies h = a * f )

assume for x being Element of NAT holds h9 . x = a * (f9 . x) ; :: thesis: h = a * f
then h1 = a * f1 by A1, FUNCSDOM:4;
hence h = a * f by A0, LM17; :: thesis: verum

end;

hence ( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) ) by A3; :: thesis: verum