set X = Big_Oh_poly ;
set m = (RealFuncMult NAT) || Big_Oh_poly;
set a = (RealFuncAdd NAT) || Big_Oh_poly;
set E = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:];
set O = RealFuncUnit NAT;
set Z = RealFuncZero NAT;
for x being set st x in [:Big_Oh_poly,Big_Oh_poly:] holds
(RealFuncMult NAT) . x in Big_Oh_poly

proof

let x be set ; :: thesis: ( x in [:Big_Oh_poly,Big_Oh_poly:] implies (RealFuncMult NAT) . x in Big_Oh_poly )
assume x in [:Big_Oh_poly,Big_Oh_poly:] ; :: thesis: (RealFuncMult NAT) . x in Big_Oh_poly
then consider f, g being object such that
B2: ( f in Big_Oh_poly & g in Big_Oh_poly & x = [f,g] ) by ZFMISC_1:def 2;
reconsider f = f, g = g as polynomially-abs-bounded Function of NAT,REAL by DefX1, B2;
set h = (RealFuncMult NAT) . x;
reconsider f1 = f, g1 = g as Element of Funcs (NAT,REAL) by FUNCT_2:8;
B5: (RealFuncMult NAT) . x = (RealFuncMult NAT) . (f1,g1) by B2;
reconsider h = (RealFuncMult NAT) . x as Function of NAT,REAL by B5;
h = f (#) g

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: h . n = (f (#) g) . n
thus h . n = (f . n) * (g . n) by B5, FUNCSDOM:2
.= (f (#) g) . n by VALUED_1:5 ; :: thesis: verum

end;

hence (RealFuncMult NAT) . x in Big_Oh_poly by DefX1; :: thesis: verum

end;

then Big_Oh_poly is Preserv of RealFuncMult NAT by REALSET1:def 1;
then reconsider m = (RealFuncMult NAT) || Big_Oh_poly as BinOp of Big_Oh_poly by REALSET1:2;
for x being set st x in [:Big_Oh_poly,Big_Oh_poly:] holds
(RealFuncAdd NAT) . x in Big_Oh_poly

proof

let x be set ; :: thesis: ( x in [:Big_Oh_poly,Big_Oh_poly:] implies (RealFuncAdd NAT) . x in Big_Oh_poly )
assume x in [:Big_Oh_poly,Big_Oh_poly:] ; :: thesis: (RealFuncAdd NAT) . x in Big_Oh_poly
then consider f, g being object such that
B2: ( f in Big_Oh_poly & g in Big_Oh_poly & x = [f,g] ) by ZFMISC_1:def 2;
reconsider f = f, g = g as polynomially-abs-bounded Function of NAT,REAL by DefX1, B2;
set h = (RealFuncAdd NAT) . x;
reconsider f1 = f, g1 = g as Element of Funcs (NAT,REAL) by FUNCT_2:8;
B5: (RealFuncAdd NAT) . x = (RealFuncAdd NAT) . (f1,g1) by B2;
then reconsider h = (RealFuncAdd NAT) . x as Function of NAT,REAL ;
h = f + g

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: h . n = (f + g) . n
thus h . n = (f . n) + (g . n) by B5, FUNCSDOM:1
.= (f + g) . n by VALUED_1:1 ; :: thesis: verum

end;

hence (RealFuncAdd NAT) . x in Big_Oh_poly by DefX1; :: thesis: verum

end;

then Big_Oh_poly is Preserv of RealFuncAdd NAT by REALSET1:def 1;
then reconsider a = (RealFuncAdd NAT) || Big_Oh_poly as BinOp of Big_Oh_poly by REALSET1:2;
Q0: [:REAL,Big_Oh_poly:] c= [:REAL,(Funcs (NAT,REAL)):] by ZFMISC_1:95;
[:REAL,(Funcs (NAT,REAL)):] = dom (RealFuncExtMult NAT) by FUNCT_2:def 1;
then Q1: dom ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) = [:REAL,Big_Oh_poly:] by RELAT_1:62, Q0;
for h being object st h in rng ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) holds
h in Big_Oh_poly

proof

let h be object ; :: thesis: ( h in rng ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) implies h in Big_Oh_poly )
assume h in rng ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) ; :: thesis: h in Big_Oh_poly
then consider x being object such that
Q2: ( x in dom ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) & h = ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) . x ) by FUNCT_1:def 3;
consider s, f being object such that
B2: ( s in REAL & f in Big_Oh_poly ) and
B3: x = [s,f] by Q1, Q2, ZFMISC_1:def 2;
reconsider f = f as polynomially-abs-bounded Function of NAT,REAL by DefX1, B2;
reconsider s = s as Element of REAL by B2;
H1: h = (RealFuncExtMult NAT) . x by Q1, Q2, FUNCT_1:49;
reconsider f1 = f as Element of Funcs (NAT,REAL) by FUNCT_2:8;
reconsider h1 = h as Element of Funcs (NAT,REAL) by H1, FUNCT_2:5, Q2;
reconsider h1 = h1 as Function of NAT,REAL ;
h1 = s (#) f

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: h1 . n = (s (#) f) . n
thus h1 . n = s * (f1 . n) by B3, H1, FUNCSDOM:4
.= (s (#) f) . n by VALUED_1:6 ; :: thesis: verum

end;

hence h in Big_Oh_poly by DefX1; :: thesis: verum

end;

then rng ((RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:]) c= Big_Oh_poly ;
then reconsider E = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] as Function of [:REAL,Big_Oh_poly:],Big_Oh_poly by Q1, FUNCT_2:2;
reconsider O = RealFuncUnit NAT as Real_Sequence ;
( O in Funcs (NAT,REAL) & seq_id O is polynomially-abs-bounded ) by LM1;
then reconsider O = O as Element of Big_Oh_poly by DefX1;
reconsider Z = RealFuncZero NAT as Real_Sequence ;
( Z in Funcs (NAT,REAL) & seq_id Z is polynomially-abs-bounded ) by LM1;
then reconsider Z = Z as Element of Big_Oh_poly by DefX1;
set S = AlgebraStr(# Big_Oh_poly,m,a,E,O,Z #);
AlgebraStr(# Big_Oh_poly,m,a,E,O,Z #) is strict AlgebraStr ;
hence ( ex b₁ being strict AlgebraStr st
( the carrier of b₁ = Big_Oh_poly & the multF of b₁ = (RealFuncMult NAT) || Big_Oh_poly & the addF of b₁ = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b₁ = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b₁ = RealFuncUnit NAT & the ZeroF of b₁ = RealFuncZero NAT ) & ( for b₁, b₂ being strict AlgebraStr st the carrier of b₁ = Big_Oh_poly & the multF of b₁ = (RealFuncMult NAT) || Big_Oh_poly & the addF of b₁ = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b₁ = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b₁ = RealFuncUnit NAT & the ZeroF of b₁ = RealFuncZero NAT & the carrier of b₂ = Big_Oh_poly & the multF of b₂ = (RealFuncMult NAT) || Big_Oh_poly & the addF of b₂ = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b₂ = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b₂ = RealFuncUnit NAT & the ZeroF of b₂ = RealFuncZero NAT holds
b₁ = b₂ ) ) ; :: thesis: verum