thus RLS_Real is Abelian :: thesis: ( RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof

let v, w be VECTOR of RLS_Real; :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider vr = v as Real ;
reconsider wr = w as Real ;
thus v + w = vr + wr by BINOP_2:def 9
.= w + v by BINOP_2:def 9 ; :: thesis: verum

end;

thus RLS_Real is add-associative :: thesis: ( RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof

let u, v, w be VECTOR of RLS_Real; :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
reconsider ur = u as Real ;
reconsider vr = v as Real ;
reconsider wr = w as Real ;
v + w = vr + wr by BINOP_2:def 9;
then A1: u + (v + w) = ur + (vr + wr) by BINOP_2:def 9;
u + v = ur + vr by BINOP_2:def 9;
then (u + v) + w = (ur + vr) + wr by BINOP_2:def 9;
hence (u + v) + w = u + (v + w) by A1; :: thesis: verum

end;

thus RLS_Real is right_zeroed :: thesis: ( RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof

let v be VECTOR of RLS_Real; :: according to RLVECT_1:def 4 :: thesis: v + (0. RLS_Real) = v
reconsider vr = v as Real ;
thus v + (0. RLS_Real) = vr + 0 by BINOP_2:def 9
.= v ; :: thesis: verum

end;

thus RLS_Real is right_complementable :: thesis: ( RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof

let v be VECTOR of RLS_Real; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider vr = v as Real ;
reconsider w = - vr as VECTOR of RLS_Real by XREAL_0:def 1;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. RLS_Real
thus v + w = vr + (- vr) by BINOP_2:def 9
.= 0. RLS_Real ; :: thesis: verum

end;

thus for a being Real
for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def 5 :: thesis: ( RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof

let a be Real; :: thesis: for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real ;
let v, w be VECTOR of RLS_Real; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider vr = v as Real ;
reconsider wr = w as Real ;
A2: a * v = a * vr by BINOP_2:def 11;
A3: a * w = a * wr by BINOP_2:def 11;
v + w = vr + wr by BINOP_2:def 9;
then a * (v + w) = a * (vr + wr) by BINOP_2:def 11
.= (a * vr) + (a * wr)
.= (a * v) + (a * w) by A2, A3, BINOP_2:def 9 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

thus for a, b being Real
for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def 6 :: thesis: ( RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof

let a, b be Real; :: thesis: for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real ;
let v be VECTOR of RLS_Real; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider vr = v as Real ;
A4: b * v = b * vr by BINOP_2:def 11;
a * v = a * vr by BINOP_2:def 11;
then (a * v) + (b * v) = (a * vr) + (b * vr) by A4, BINOP_2:def 9
.= (a + b) * vr
.= (a + b) * v by BINOP_2:def 11 ;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

thus for a, b being Real
for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def 7 :: thesis: RLS_Real is scalar-unital

proof

let a, b be Real; :: thesis: for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real ;
let v be VECTOR of RLS_Real; :: thesis: (a * b) * v = a * (b * v)
reconsider vr = v as Real ;
b * v = b * vr by BINOP_2:def 11;
then a * (b * v) = a * (b * vr) by BINOP_2:def 11
.= (a * b) * vr
.= (a * b) * v by BINOP_2:def 11 ;
hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of RLS_Real; :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
reconsider vr = v as Real ;
thus 1 * v = 1 * vr by BINOP_2:def 11
.= v ; :: thesis: verum