let f, g, h be VECTOR of R_Algebra_of_Big_Oh_poly; :: thesis: for f9, g9, h9 being Function of NAT,REAL st f9 = f & g9 = g & h9 = h holds
( h = f * g iff for x being Nat holds h9 . x = (f9 . x) * (g9 . x) )
reconsider f1 = f, g1 = g, h1 = h as VECTOR of (RAlgebra NAT) by LM12;
let f9, g9, h9 be Function of NAT,REAL; :: thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f * g iff for x being Nat holds h9 . x = (f9 . x) * (g9 . x) ) )
assume A2: ( f9 = f & g9 = g & h9 = h ) ; :: thesis: ( h = f * g iff for x being Nat holds h9 . x = (f9 . x) * (g9 . x) )

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

assume A4: h = f * g ; :: thesis: for x being Nat holds h9 . x = (f9 . x) * (g9 . x)
let x be Nat; :: thesis: h9 . x = (f9 . x) * (g9 . x)
LXN: x in NAT by ORDINAL1:def 12;
h1 = f1 * g1 by A4, LM15;
hence h9 . x = (f9 . x) * (g9 . x) by A2, FUNCSDOM:2, LXN; :: thesis: verum

end;

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

assume for x being Element of NAT holds h9 . x = (f9 . x) * (g9 . x) ; :: thesis: h = f * g
then h1 = f1 * g1 by A2, FUNCSDOM:2;
hence h = f * g by LM15; :: thesis: verum

end;

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