let X, Y be RealLinearSpace; :: thesis: 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)); :: thesis: ( 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) ; :: thesis: v + u in LinearOperators (X,Y)
v + u is LinearOperator of X,Y

proof

reconsider f = v + u as Function of X,Y by FUNCT_2:66;
A4: f is homogeneous

proof

reconsider v9 = v, u9 = u as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x be VECTOR of X; :: according to LOPBAN_1:def 5 :: thesis: for r being Real holds f . (r * x) = r * (f . x)
let s be Real; :: thesis: f . (s * x) = s * (f . x)
A5: u9 is LinearOperator of X,Y by A3, Def7;
A6: v9 is LinearOperator of X,Y by A2, Def7;
thus f . (s * x) = (u9 . (s * x)) + (v9 . (s * x)) by Th3
.= (s * (u9 . x)) + (v9 . (s * x)) by A5, Def6
.= (s * (u9 . x)) + (s * (v9 . x)) by A6, Def6
.= s * ((u9 . x) + (v9 . x)) by RLVECT_1:def 5
.= s * (f . x) by Th3 ; :: thesis: verum

end;

f is additive

proof

reconsider v9 = v, u9 = u as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x, y be VECTOR of X; :: according to GRCAT_1:def 8 :: thesis: f . (x + y) = (f . x) + (f . y)
A7: u9 is LinearOperator of X,Y by A3, Def7;
A8: v9 is LinearOperator of X,Y by A2, Def7;
thus f . (x + y) = (u9 . (x + y)) + (v9 . (x + y)) by Th3
.= ((u9 . x) + (u9 . y)) + (v9 . (x + y)) by A7, GRCAT_1:def 8
.= ((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y)) by A8, GRCAT_1:def 8
.= (((u9 . x) + (u9 . y)) + (v9 . x)) + (v9 . y) by RLVECT_1:def 3
.= (((u9 . x) + (v9 . x)) + (u9 . y)) + (v9 . y) by RLVECT_1:def 3
.= ((f . x) + (u9 . y)) + (v9 . y) by Th3
.= (f . x) + ((u9 . y) + (v9 . y)) by RLVECT_1:def 3
.= (f . x) + (f . y) by Th3 ; :: thesis: verum

end;

hence v + u is LinearOperator of X,Y by A4; :: thesis: verum

end;

hence v + u in LinearOperators (X,Y) by Def7; :: thesis: 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; :: thesis: 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)); :: thesis: ( v in LinearOperators (X,Y) implies a * v in LinearOperators (X,Y) )
assume A9: v in LinearOperators (X,Y) ; :: thesis: a * v in LinearOperators (X,Y)
a * v is LinearOperator of X,Y

proof

reconsider f = a * v as Function of X,Y by FUNCT_2:66;
A10: f is homogeneous

proof

reconsider v9 = v as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x be VECTOR of X; :: according to LOPBAN_1:def 5 :: thesis: for r being Real holds f . (r * x) = r * (f . x)
let s be Real; :: thesis: f . (s * x) = s * (f . x)
A11: v9 is LinearOperator of X,Y by A9, Def7;
thus f . (s * x) = a * (v9 . (s * x)) by Th5
.= a * (s * (v9 . x)) by A11, Def6
.= (a * s) * (v9 . x) by RLVECT_1:def 7
.= s * (a * (v9 . x)) by RLVECT_1:def 7
.= s * (f . x) by Th5 ; :: thesis: verum

end;

f is additive

proof

reconsider v9 = v as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x, y be VECTOR of X; :: according to GRCAT_1:def 8 :: thesis: f . (x + y) = (f . x) + (f . y)
A12: v9 is LinearOperator of X,Y by A9, Def7;
thus f . (x + y) = a * (v9 . (x + y)) by Th5
.= a * ((v9 . x) + (v9 . y)) by A12, GRCAT_1:def 8
.= (a * (v9 . x)) + (a * (v9 . y)) by RLVECT_1:def 5
.= (f . x) + (a * (v9 . y)) by Th5
.= (f . x) + (f . y) by Th5 ; :: thesis: verum

end;

hence a * v is LinearOperator of X,Y by A10; :: thesis: verum

end;

hence a * v in LinearOperators (X,Y) by Def7; :: thesis: verum

end;

hence LinearOperators (X,Y) is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum