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, LM16;
hence h9 . x = (f9 . x) + (g9 . x) by A2, FUNCSDOM:1, LXN; :: thesis: verum

end;

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

assume LAS: for x being Nat holds h9 . x = (f9 . x) + (g9 . x) ; :: thesis: h = f + g
for x being Element of NAT holds h9 . x = (f9 . x) + (g9 . x) by LAS;
then h1 = f1 + g1 by A2, FUNCSDOM:1;
hence h = f + g by LM16; :: thesis: verum

end;

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