let X be non empty set ; :: thesis: for Y being RealLinearSpace holds RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
let Y be RealLinearSpace; :: thesis: RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
A1: for a, b being real number
for v being VECTOR of holds (a * b) * v = a * (b * v)

proof

let a, b be real number ; :: thesis: for v being VECTOR of holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
for v being VECTOR of holds (a * b) * v = a * (b * v) by Th11;
hence for v being VECTOR of holds (a * b) * v = a * (b * v) ; :: thesis: verum

end;

A2: for a, b being real number
for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)

proof

let a, b be real number ; :: thesis: for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
for v being VECTOR of holds (a + b) * v = (a * v) + (b * v) by Th12;
hence for v being VECTOR of holds (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

set IT = RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);
A3: for u, v, w being VECTOR of holds (u + v) + w = u + (v + w) by Th7;
A4: RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable

proof

let u be VECTOR of ; :: according to ALGSTR_0:def 16 :: thesis: u is right_complementable
reconsider u' = u as Element of Funcs X,the carrier of Y ;
reconsider w = (FuncExtMult X,Y) . [(- 1),u'] as VECTOR of ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: u + w = 0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)
thus u + w = 0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) by Th9; :: thesis: verum

end;

A5: for a being real number
for u, v being VECTOR of holds a * (u + v) = (a * u) + (a * v)

proof

let a be real number ; :: thesis: for u, v being VECTOR of holds a * (u + v) = (a * u) + (a * v)
reconsider a = a as Real by XREAL_0:def 1;
for u, v being VECTOR of holds a * (u + v) = (a * u) + (a * v) by Lm2;
hence for u, v being VECTOR of holds a * (u + v) = (a * u) + (a * v) ; :: thesis: verum

end;

A6: for v being VECTOR of holds 1 * v = v by Th10;
A7: for u being VECTOR of holds u + (0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) = u

proof

let u be VECTOR of ; :: thesis: u + (0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) = u
reconsider u' = u as Element of Funcs X,the carrier of Y ;
thus u + (0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) = (FuncAdd X,Y) . (FuncZero X,Y),u' by Th6
.= u by Th8 ; :: thesis: verum

end;

for u, v being VECTOR of holds u + v = v + u by Th6;
hence RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace by A3, A7, A4, A5, A2, A1, A6, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 9; :: thesis: verum