set S = R_Algebra_of_Big_Oh_poly ;
thus
R_Algebra_of_Big_Oh_poly is strict
; ( 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
( 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 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 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 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 )
for x, y being Element of R_Algebra_of_Big_Oh_poly holds x * y = y * x
hence
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 )
for x, y, z being Element of R_Algebra_of_Big_Oh_poly holds (x * y) * z = x * (y * z)
hence
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 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) + (x * z)
hence
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 being Element of R_Algebra_of_Big_Oh_poly
for s being Real holds s * (x * y) = (s * x) * y
hence
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 s, t being Real
for x being Element of R_Algebra_of_Big_Oh_poly holds (s * t) * x = s * (t * x)
hence
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 being Real
for x, y being Element of R_Algebra_of_Big_Oh_poly holds s * (x + y) = (s * x) + (s * y)
hence
R_Algebra_of_Big_Oh_poly is vector-distributive
; R_Algebra_of_Big_Oh_poly is scalar-distributive
let s, t be Real; RLVECT_1:def 6 for b1 being Element of the carrier of R_Algebra_of_Big_Oh_poly holds (s + t) * b1 = (s * b1) + (t * b1)
let v be Element of R_Algebra_of_Big_Oh_poly; (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)
; verum