thus RLS_Real is Abelian :: thesis: ( RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is RealLinearSpace-like )

proof

let v, w be VECTOR of RLS_Real ; :: according to RLVECT_1:def 5 :: 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 RealLinearSpace-like )

proof

let u, v, w be VECTOR of RLS_Real ; :: according to RLVECT_1:def 6 :: thesis: (u + v) + w = u + (v + w)
reconsider ur = u as Real ;
reconsider vr = v as Real ;
reconsider wr = w as Real ;
u + v = ur + vr by BINOP_2:def 9;
then A1: (u + v) + w = (ur + vr) + wr by BINOP_2:def 9;
v + w = vr + wr 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 RealLinearSpace-like )

proof

let v be VECTOR of RLS_Real ; :: according to RLVECT_1:def 7 :: 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 RealLinearSpace-like

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 ;
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 9 :: thesis: ( ( for b₁, b₂ being Element of REAL
for b₃ being Element of the carrier of RLS_Real holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being Element of REAL
for b₃ being Element of the carrier of RLS_Real holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of RLS_Real holds 1 * b₁ = b₁ ) )

proof

let a be Real; :: thesis: for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w)
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 & a * w = a * wr ) by BINOP_2:def 11;
v + w = vr + wr by BINOP_2:def 9;
hence a * (v + w) = a * (vr + wr) by BINOP_2:def 11
.= (a * vr) + (a * wr)
.= (a * v) + (a * w) by A2, BINOP_2:def 9 ;
:: thesis: verum

end;

thus for a, b being Real
for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v) :: thesis: ( ( for b₁, b₂ being Element of REAL
for b₃ being Element of the carrier of RLS_Real holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of RLS_Real holds 1 * b₁ = b₁ ) )

proof

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

end;

thus for a, b being Real
for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v) :: thesis: for b₁ being Element of the carrier of RLS_Real holds 1 * b₁ = b₁

proof

let a, b be Real; :: thesis: for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v)
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;
hence a * (b * v) = a * (b * vr) by BINOP_2:def 11
.= (a * b) * vr
.= (a * b) * v by BINOP_2:def 11 ;
:: thesis: verum

end;

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