thus RAlgebra A is strict ; :: thesis:
thus RAlgebra A is Abelian :: thesis:

proof

let x, y be Element of (RAlgebra A); :: according to RLVECT_1:def 2 :: thesis:
thus x + y = y + x by Th16; :: thesis:

end;

thus RAlgebra A is add-associative :: thesis:

proof

let x, y, z be Element of (RAlgebra A); :: according to RLVECT_1:def 3 :: thesis:
thus (x + y) + z = x + (y + z) by Th17; :: thesis:

end;

thus RAlgebra A is right_zeroed :: thesis:

proof

let x be Element of (RAlgebra A); :: according to RLVECT_1:def 4 :: thesis:
thus x + (0. (RAlgebra A)) = (RealFuncAdd A) . ((RealFuncZero A),x) by Th16
.= x by Th21 ; :: thesis:

end;

thus RAlgebra A is right_complementable :: thesis:

proof

let x be Element of (RAlgebra A); :: according to ALGSTR_0:def 16 :: thesis:
reconsider f = x as Element of Funcs (A,REAL) ;
reconsider t = (RealFuncExtMult A) . [(- 1),f] as Element of (RAlgebra A) ;
take t ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + t = 0. (RAlgebra A) by Th22; :: thesis:

end;

thus RAlgebra A is commutative :: thesis:

proof

let x, y be Element of (RAlgebra A); :: according to GROUP_1:def 12 :: thesis:
thus x * y = y * x by Th18; :: thesis:

end;

thus RAlgebra A is associative :: thesis:

proof

let x, y, z be Element of (RAlgebra A); :: according to GROUP_1:def 3 :: thesis:
thus (x * y) * z = x * (y * z) by Th19; :: thesis:

end;

thus RAlgebra A is right_unital :: thesis:

proof

let x be Element of (RAlgebra A); :: according to VECTSP_1:def 4 :: thesis:
thus x * (1. (RAlgebra A)) = (RealFuncMult A) . ((RealFuncUnit A),x) by Th18
.= x by Th20 ; :: thesis:

end;

thus RAlgebra A is right-distributive :: thesis:

proof

let x, y, z be Element of (RAlgebra A); :: according to VECTSP_1:def 2 :: thesis:
thus x * (y + z) = (x * y) + (x * z) by Th26; :: thesis:

end;

thus RAlgebra A is vector-associative :: thesis:

proof

let x, y be Element of (RAlgebra A); :: according to FUNCSDOM:def 9 :: thesis:
let a be Real; :: thesis:
thus (a * x) * y = a * (x * y) by Th27; :: thesis:

end;

thus RAlgebra A is scalar-associative :: thesis:

proof

let a, b be real number ; :: according to RLVECT_1:def 7 :: thesis:
let x be Element of (RAlgebra A); :: thesis:
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
(a * b) * x = a * (b * x) by Th24;
hence (a * b) * x = a * (b * x) ; :: thesis:

end;

thus RAlgebra A is vector-distributive :: thesis:

proof

let a be real number ; :: according to RLVECT_1:def 5 :: thesis:
let v, w be Element of (RAlgebra A); :: thesis:
reconsider a = a as Element of REAL by XREAL_0:def 1;
a * (v + w) = (a * v) + (a * w) by Lm2;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis:

end;

let a, b be real number ; :: according to RLVECT_1:def 6 :: thesis:
let v be Element of (RAlgebra A); :: thesis:
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
(a + b) * v = (a * v) + (b * v) by Th25;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: