let X be non empty set ; 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; RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace
A1:
for a, b being Real
for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a * b) * v = a * (b * v)
by Th8;
A2:
for a, b being Real
for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a + b) * v = (a * v) + (b * v)
by Th9;
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 RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (u + v) + w = u + (v + w)
by Th4;
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
RLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #);
ALGSTR_0:def 16 u is right_complementable
reconsider u9 =
u as
Element of
Funcs (
X, the
carrier of
Y) ;
reconsider w =
(FuncExtMult (X,Y)) . [(- jj),u9] as
VECTOR of
RLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #) ;
take
w
;
ALGSTR_0:def 11 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 Th6;
verum
end;
A5:
for a being Real
for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds a * (u + v) = (a * u) + (a * v)
by Lm2;
A6:
for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds 1 * v = v
by Th7;
A7:
for u being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) 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
RLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #);
u + (0. RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)) = u
reconsider u9 =
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)),
u9)
by Th3
.=
u
by Th5
;
verum
end;
for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds u + v = v + u
by Th3;
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 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8; verum