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) #);
ALGSTR_0:def 16 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
;
ALGSTR_0:def 11 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;
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) #);
RLVECT_1:def 4 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
;
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; verum