set S = RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #);
A1: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is add-associative

proof

let u, v, w be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
thus (u + v) + w = u + (v + w) by Th17; :: thesis: verum

end;

A2: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is right_complementable

proof

let u be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to ALGSTR_0:def 16 :: thesis: u is right_complementable
reconsider u9 = u as Element of Funcs (A,REAL) ;
reconsider w = (RealFuncExtMult A) . [(- 1),u9] as VECTOR of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: u + w = 0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)
thus u + w = 0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) by Th22; :: thesis: verum

end;

A3: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is vector-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital )

proof

thus for a being real number
for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def 5 :: thesis: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-distributive & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital )

proof

let a be real number ; :: thesis: for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real by XREAL_0:def 1;
for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) by Lm2;
hence for v, w being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

thus for a, b being real number
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def 6 :: thesis: ( RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-associative & RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital )

proof

let a, b be real number ; :: thesis: for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) by Th25;
hence for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

thus for a, b being real number
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def 7 :: thesis: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is scalar-unital

proof

let a, b be real number ; :: thesis: for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) by Th24;
hence for v being Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) holds (a * b) * v = a * (b * v) ; :: thesis: verum

end;

let v be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
thus 1 * v = v by Th23; :: thesis: verum

end;

A4: RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is right_zeroed

proof

let u be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def 4 :: thesis: u + (0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)) = u
reconsider u9 = u as Element of Funcs (A,REAL) ;
thus u + (0. RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #)) = (RealFuncAdd A) . ((RealFuncZero A),u9) by Th16
.= u by Th21 ; :: thesis: verum

end;

RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is Abelian

proof

let u, v be Element of RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #); :: according to RLVECT_1:def 2 :: thesis: u + v = v + u
thus u + v = v + u by Th16; :: thesis: verum

end;

hence RLSStruct(# (Funcs (A,REAL)),(RealFuncZero A),(RealFuncAdd A),(RealFuncExtMult A) #) is strict RealLinearSpace by A1, A4, A2, A3; :: thesis: verum