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 )

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 )

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 )

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

reconsider vr = v as Real ;

thus 1 * v = 1 * vr by BINOP_2:def 11

.= v ; :: thesis: verum

proof

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 )
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;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

proof

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 )
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;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

proof

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 )
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;reconsider vr = v as Real ;

thus v + (0. RLS_Real) = vr + 0 by BINOP_2:def 9

.= v ; :: thesis: verum

proof

thus
for a being Real
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;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

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

thus
for a, b being Real
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;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

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

thus
for a, b being Real
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;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

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 v be VECTOR of RLS_Real; :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
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;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

reconsider vr = v as Real ;

thus 1 * v = 1 * vr by BINOP_2:def 11

.= v ; :: thesis: verum