let X, Y be RealLinearSpace; LinearOperators (X,Y) is linearly-closed
set W = LinearOperators (X,Y);
A1:
for v, u being VECTOR of (RealVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) & u in LinearOperators (X,Y) holds
v + u in LinearOperators (X,Y)
proof
let v,
u be
VECTOR of
(RealVectSpace ( the carrier of X,Y));
( v in LinearOperators (X,Y) & u in LinearOperators (X,Y) implies v + u in LinearOperators (X,Y) )
assume that A2:
v in LinearOperators (
X,
Y)
and A3:
u in LinearOperators (
X,
Y)
;
v + u in LinearOperators (X,Y)
v + u is
LinearOperator of
X,
Y
hence
v + u in LinearOperators (
X,
Y)
by Def6;
verum
end;
for a being Real
for v being VECTOR of (RealVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds
a * v in LinearOperators (X,Y)
proof
let a be
Real;
for v being VECTOR of (RealVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds
a * v in LinearOperators (X,Y)let v be
VECTOR of
(RealVectSpace ( the carrier of X,Y));
( v in LinearOperators (X,Y) implies a * v in LinearOperators (X,Y) )
assume A9:
v in LinearOperators (
X,
Y)
;
a * v in LinearOperators (X,Y)
a * v is
LinearOperator of
X,
Y
hence
a * v in LinearOperators (
X,
Y)
by Def6;
verum
end;
hence
LinearOperators (X,Y) is linearly-closed
by A1, RLSUB_1:def 1; verum