set S = R_Algebra_of_Big_Oh_poly ;
thus R_Algebra_of_Big_Oh_poly is strict ; :: thesis: ( R_Algebra_of_Big_Oh_poly is Abelian & R_Algebra_of_Big_Oh_poly is add-associative & R_Algebra_of_Big_Oh_poly is right_zeroed & R_Algebra_of_Big_Oh_poly is right_complementable & R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )
thus R_Algebra_of_Big_Oh_poly is Abelian :: thesis: ( R_Algebra_of_Big_Oh_poly is add-associative & R_Algebra_of_Big_Oh_poly is right_zeroed & R_Algebra_of_Big_Oh_poly is right_complementable & R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )

proof

let x, y be Element of R_Algebra_of_Big_Oh_poly; :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of (RAlgebra NAT) by LM12;
thus x + y = x1 + y1 by LM16
.= y + x by LM16 ; :: thesis: verum

end;

thus R_Algebra_of_Big_Oh_poly is add-associative :: thesis: ( R_Algebra_of_Big_Oh_poly is right_zeroed & R_Algebra_of_Big_Oh_poly is right_complementable & R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )

proof

let x, y, z be Element of R_Algebra_of_Big_Oh_poly; :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of (RAlgebra NAT) by LM12;
D1: x + y = x1 + y1 by LM16;
D2: y + z = y1 + z1 by LM16;
thus (x + y) + z = (x1 + y1) + z1 by D1, LM16
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= x + (y + z) by D2, LM16 ; :: thesis: verum

end;

thus R_Algebra_of_Big_Oh_poly is right_zeroed :: thesis: ( R_Algebra_of_Big_Oh_poly is right_complementable & R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )

proof

let x be Element of R_Algebra_of_Big_Oh_poly; :: according to RLVECT_1:def 4 :: thesis: x + (0. R_Algebra_of_Big_Oh_poly) = x
reconsider x1 = x as Element of (RAlgebra NAT) by LM12;
thus x + (0. R_Algebra_of_Big_Oh_poly) = x1 + (0. (RAlgebra NAT)) by LM18, LM16
.= x ; :: thesis: verum

end;

thus R_Algebra_of_Big_Oh_poly is right_complementable :: thesis: ( R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )

proof

let x be Element of R_Algebra_of_Big_Oh_poly; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as Element of (RAlgebra NAT) by LM12;
set t1 = (- 1) * x;
take (- 1) * x ; :: according to ALGSTR_0:def 11 :: thesis: x + ((- 1) * x) = 0. R_Algebra_of_Big_Oh_poly
- 1 is Element of REAL by XREAL_0:def 1;
then D1: (- 1) * x = (- 1) * x1 by LM17;
thus x + ((- 1) * x) = x1 + ((- 1) * x1) by D1, LM16
.= 0. (RAlgebra NAT) by FUNCSDOM:11
.= 0. R_Algebra_of_Big_Oh_poly by defAlgebra ; :: thesis: verum

end;

for x, y being Element of R_Algebra_of_Big_Oh_poly holds x * y = y * x

proof

let x, y be Element of R_Algebra_of_Big_Oh_poly; :: thesis: x * y = y * x
reconsider x1 = x, y1 = y as Element of (RAlgebra NAT) by LM12;
thus x * y = x1 * y1 by LM15
.= y * x by LM15 ; :: thesis: verum

end;

hence R_Algebra_of_Big_Oh_poly is commutative ; :: thesis: ( R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )
for x, y, z being Element of R_Algebra_of_Big_Oh_poly holds (x * y) * z = x * (y * z)

proof

let x, y, z be Element of R_Algebra_of_Big_Oh_poly; :: thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of (RAlgebra NAT) by LM12;
D1: x * y = x1 * y1 by LM15;
D2: y * z = y1 * z1 by LM15;
thus (x * y) * z = (x1 * y1) * z1 by D1, LM15
.= x1 * (y1 * z1) by GROUP_1:def 3
.= x * (y * z) by D2, LM15 ; :: thesis: verum

end;

hence R_Algebra_of_Big_Oh_poly is associative ; :: thesis: ( R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )
thus R_Algebra_of_Big_Oh_poly is right_unital :: thesis: ( R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )

proof

let x be Element of R_Algebra_of_Big_Oh_poly; :: according to VECTSP_1:def 4 :: thesis: x * (1. R_Algebra_of_Big_Oh_poly) = x
reconsider x1 = x as Element of (RAlgebra NAT) by LM12;
thus x * (1. R_Algebra_of_Big_Oh_poly) = x1 * (1. (RAlgebra NAT)) by LM19, LM15
.= x by VECTSP_1:def 4 ; :: thesis: verum

end;

for x, y, z being Element of R_Algebra_of_Big_Oh_poly holds x * (y + z) = (x * y) + (x * z)

proof

let x, y, z be Element of R_Algebra_of_Big_Oh_poly; :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of (RAlgebra NAT) by LM12;
D1: x * y = x1 * y1 by LM15;
D2: x * z = x1 * z1 by LM15;
D3: y + z = y1 + z1 by LM16;
thus x * (y + z) = x1 * (y1 + z1) by D3, LM15
.= (x1 * y1) + (x1 * z1) by VECTSP_1:def 2
.= (x * y) + (x * z) by D1, D2, LM16 ; :: thesis: verum

end;

hence R_Algebra_of_Big_Oh_poly is right-distributive ; :: thesis: ( R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )
for x, y being Element of R_Algebra_of_Big_Oh_poly
for s being Real holds s * (x * y) = (s * x) * y

proof

let x, y be Element of R_Algebra_of_Big_Oh_poly; :: thesis: for s being Real holds s * (x * y) = (s * x) * y
let s be Real; :: thesis: s * (x * y) = (s * x) * y
reconsider x1 = x, y1 = y as Element of (RAlgebra NAT) by LM12;
D1: x * y = x1 * y1 by LM15;
D3: s is Element of REAL by XREAL_0:def 1;
then D2: s * x = s * x1 by LM17;
thus s * (x * y) = s * (x1 * y1) by LM17, D1, D3
.= (s * x1) * y1 by FUNCSDOM:def 9
.= (s * x) * y by LM15, D2 ; :: thesis: verum

end;

hence R_Algebra_of_Big_Oh_poly is vector-associative ; :: thesis: ( R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )
for s, t being Real
for x being Element of R_Algebra_of_Big_Oh_poly holds (s * t) * x = s * (t * x)

proof

let s, t be Real; :: thesis: for x being Element of R_Algebra_of_Big_Oh_poly holds (s * t) * x = s * (t * x)
let x be Element of R_Algebra_of_Big_Oh_poly; :: thesis: (s * t) * x = s * (t * x)
reconsider x1 = x as Element of (RAlgebra NAT) by LM12;
D0: ( s is Element of REAL & t is Element of REAL ) by XREAL_0:def 1;
D2: s * t is Element of REAL by XREAL_0:def 1;
D1: t * x = t * x1 by D0, LM17;
thus (s * t) * x = (s * t) * x1 by D2, LM17
.= s * (t * x1) by RLVECT_1:def 7
.= s * (t * x) by D0, D1, LM17 ; :: thesis: verum

end;

hence R_Algebra_of_Big_Oh_poly is scalar-associative ; :: thesis: ( R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive )
for s being Real
for x, y being Element of R_Algebra_of_Big_Oh_poly holds s * (x + y) = (s * x) + (s * y)

proof

let s be Real; :: thesis: for x, y being Element of R_Algebra_of_Big_Oh_poly holds s * (x + y) = (s * x) + (s * y)
let x, y be Element of R_Algebra_of_Big_Oh_poly; :: thesis: s * (x + y) = (s * x) + (s * y)
reconsider x1 = x, y1 = y as Element of (RAlgebra NAT) by LM12;
D1: x + y = x1 + y1 by LM16;
D3: s is Element of REAL by XREAL_0:def 1;
then D2: s * x = s * x1 by LM17;
D4: s * y = s * y1 by LM17, D3;
thus s * (x + y) = s * (x1 + y1) by LM17, D1, D3
.= (s * x1) + (s * y1) by RLVECT_1:def 5
.= (s * x) + (s * y) by LM16, D2, D4 ; :: thesis: verum

end;

hence R_Algebra_of_Big_Oh_poly is vector-distributive ; :: thesis: R_Algebra_of_Big_Oh_poly is scalar-distributive
let s, t be Real; :: according to RLVECT_1:def 6 :: thesis: for b₁ being Element of the carrier of R_Algebra_of_Big_Oh_poly holds (s + t) * b₁ = (s * b₁) + (t * b₁)
let v be Element of R_Algebra_of_Big_Oh_poly; :: thesis: (s + t) * v = (s * v) + (t * v)
reconsider s = s, t = t as Element of REAL by XREAL_0:def 1;
reconsider v1 = v as Element of (RAlgebra NAT) by LM12;
D2: s * v = s * v1 by LM17;
D4: t * v = t * v1 by LM17;
(s + t) * v = (s + t) * v1 by LM17
.= (s * v1) + (t * v1) by RLVECT_1:def 6
.= (s * v) + (t * v) by D2, D4, LM16 ;
hence (s + t) * v = (s * v) + (t * v) ; :: thesis: verum