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 by Th6;
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) . [(- jj),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 Th11; :: 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 ) by Lm2, Th14, Th13, Th12;
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 Th5
.= u by Th10 ; :: thesis: verum

end;

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