let V be RealLinearSpace; :: thesis:
let V1 be Subset of V; :: thesis:
let D be non empty set ; :: thesis:
let d1 be Element of D; :: thesis:
let A be BinOp of D; :: thesis:
let M be Function of [:REAL ,D:],D; :: thesis:
assume that
A1: V1 = D and
A2: d1 = 0. V and
A3: A = the addF of V || V1 and
A4: M = the Mult of V | [:REAL ,V1:] ; :: thesis:
set W = RLSStruct(# D,d1,A,M #);
A5: 0. RLSStruct(# D,d1,A,M #) = 0. V by A2;
A6: for x, y being VECTOR of RLSStruct(# D,d1,A,M #) holds x + y = the addF of V . x,y

proof

let x, y be VECTOR of RLSStruct(# D,d1,A,M #); :: thesis:
thus x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:72
.= the addF of V . x,y ; :: thesis:

end;

A7: for a being Real
for x being VECTOR of RLSStruct(# D,d1,A,M #) holds a * x = the Mult of V . a,x

proof

let a be Real; :: thesis:
let x be VECTOR of RLSStruct(# D,d1,A,M #); :: thesis:
thus a * x = the Mult of V . [a,x] by A1, A4, FUNCT_1:72
.= the Mult of V . a,x ; :: thesis:

end;

( RLSStruct(# D,d1,A,M #) is Abelian & RLSStruct(# D,d1,A,M #) is add-associative & RLSStruct(# D,d1,A,M #) is right_zeroed & RLSStruct(# D,d1,A,M #) is right_complementable & RLSStruct(# D,d1,A,M #) is RealLinearSpace-like )

proof

set AV = the addF of V;
set MV = the Mult of V;
thus RLSStruct(# D,d1,A,M #) is Abelian :: thesis:

proof

let x, y be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def 5 :: thesis:
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
thus x + y = x1 + y1 by A6
.= y1 + x1
.= y + x by A6 ; :: thesis:

end;

thus RLSStruct(# D,d1,A,M #) is add-associative :: thesis:

proof

let x, y, z be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def 6 :: thesis:
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;
thus (x + y) + z = the addF of V . (x + y),z1 by A6
.= (x1 + y1) + z1 by A6
.= x1 + (y1 + z1) by RLVECT_1:def 6
.= the addF of V . x1,(y + z) by A6
.= x + (y + z) by A6 ; :: thesis:

end;

thus RLSStruct(# D,d1,A,M #) is right_zeroed :: thesis:

proof

let x be VECTOR of RLSStruct(# D,d1,A,M #); :: according to RLVECT_1:def 7 :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus x + (0. RLSStruct(# D,d1,A,M #)) = y + (0. V) by A2, A6
.= x by RLVECT_1:10 ; :: thesis:

end;

thus RLSStruct(# D,d1,A,M #) is right_complementable :: thesis:

proof

let x be VECTOR of RLSStruct(# D,d1,A,M #); :: according to ALGSTR_0:def 16 :: thesis:
reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;
consider v being VECTOR of V such that
A8: x1 + v = 0. V by ALGSTR_0:def 11;
v = - x1 by A8, RLVECT_1:def 11
.= (- 1) * x1 by RLVECT_1:29
.= (- 1) * x by A7 ;
then reconsider y = v as VECTOR of RLSStruct(# D,d1,A,M #) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = 0. RLSStruct(# D,d1,A,M #) by A2, A6, A8; :: thesis:

end;

thus for a being real number
for x, y being VECTOR of RLSStruct(# D,d1,A,M #) holds a * (x + y) = (a * x) + (a * y) :: according to RLVECT_1:def 9 :: thesis:

proof

let a be real number ; :: thesis:
reconsider a = a as Real by XREAL_0:def 1;
let x, y be VECTOR of RLSStruct(# D,d1,A,M #); :: thesis:
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
a * (x + y) = the Mult of V . a,(x + y) by A7
.= a * (x1 + y1) by A6
.= (a * x1) + (a * y1) by RLVECT_1:def 9
.= the addF of V . (the Mult of V . a,x1),(a * y) by A7
.= the addF of V . (a * x),(a * y) by A7
.= (a * x) + (a * y) by A6 ;
hence a * (x + y) = (a * x) + (a * y) ; :: thesis:

end;

thus for a, b being real number
for x being VECTOR of RLSStruct(# D,d1,A,M #) holds (a + b) * x = (a * x) + (b * x) :: thesis:

proof

let a, b be real number ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
let x be VECTOR of RLSStruct(# D,d1,A,M #); :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
(a + b) * x = (a + b) * y by A7
.= (a * y) + (b * y) by RLVECT_1:def 9
.= the addF of V . (the Mult of V . a,y),(b * x) by A7
.= the addF of V . (a * x),(b * x) by A7
.= (a * x) + (b * x) by A6 ;
hence (a + b) * x = (a * x) + (b * x) ; :: thesis:

end;

thus for a, b being real number
for x being VECTOR of RLSStruct(# D,d1,A,M #) holds (a * b) * x = a * (b * x) :: thesis:

proof

let a, b be real number ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
let x be VECTOR of RLSStruct(# D,d1,A,M #); :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
(a * b) * x = (a * b) * y by A7
.= a * (b * y) by RLVECT_1:def 9
.= the Mult of V . a,(b * x) by A7
.= a * (b * x) by A7 ;
hence (a * b) * x = a * (b * x) ; :: thesis:

end;

let x be VECTOR of RLSStruct(# D,d1,A,M #); :: thesis:
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus 1 * x = 1 * y by A7
.= x by RLVECT_1:def 9 ; :: thesis:

end;

hence RLSStruct(# D,d1,A,M #) is Subspace of V by A1, A3, A4, A5, Def2; :: thesis: