thus RAlgebra A is strict ; :: thesis: ( RAlgebra A is Abelian & RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is Abelian by Th5; :: thesis: ( RAlgebra A is add-associative & RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is add-associative by Th6; :: thesis: ( RAlgebra A is right_zeroed & RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is right_zeroed :: thesis: ( RAlgebra A is right_complementable & RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x be Element of (RAlgebra A); :: according to RLVECT_1:def 4 :: thesis: x + (0. (RAlgebra A)) = x
thus x + (0. (RAlgebra A)) = (RealFuncAdd A) . ((RealFuncZero A),x) by Th5
.= x by Th10 ; :: thesis: verum
end;
thus RAlgebra A is right_complementable :: thesis: ( RAlgebra A is commutative & RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x be Element of (RAlgebra A); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider f = x as Element of Funcs (A,REAL) ;
reconsider t = (RealFuncExtMult A) . [(- jj),f] as Element of (RAlgebra A) ;
take t ; :: according to ALGSTR_0:def 11 :: thesis: x + t = 0. (RAlgebra A)
thus x + t = 0. (RAlgebra A) by Th11; :: thesis: verum
end;
thus RAlgebra A is commutative by Th7; :: thesis: ( RAlgebra A is associative & RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is associative by Th8; :: thesis: ( RAlgebra A is right_unital & RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is right_unital :: thesis: ( RAlgebra A is right-distributive & RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
proof
let x be Element of (RAlgebra A); :: according to VECTSP_1:def 4 :: thesis: x * (1. (RAlgebra A)) = x
thus x * (1. (RAlgebra A)) = (RealFuncMult A) . ((RealFuncUnit A),x) by Th7
.= x by Th9 ; :: thesis: verum
end;
thus RAlgebra A is right-distributive by Th15; :: thesis: ( RAlgebra A is vector-associative & RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is vector-associative by Th16; :: thesis: ( RAlgebra A is scalar-associative & RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is scalar-associative by Th13; :: thesis: ( RAlgebra A is vector-distributive & RAlgebra A is scalar-distributive )
thus RAlgebra A is vector-distributive by Lm2; :: thesis: RAlgebra A is scalar-distributive
let a, b be Real; :: according to RLVECT_1:def 6 :: thesis: for b1 being Element of the carrier of (RAlgebra A) holds (a + b) * b1 = (a * b1) + (b * b1)
let v be Element of (RAlgebra A); :: thesis: (a + b) * v = (a * v) + (b * v)
thus (a + b) * v = (a * v) + (b * v) by Th14; :: thesis: verum