let X be RealLinearSpace; :: thesis: LinearFunctionals X is linearly-closed
set W = LinearFunctionals X;
A1: for v, u being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X & u in LinearFunctionals X holds
v + u in LinearFunctionals X

proof

let v, u be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in LinearFunctionals X & u in LinearFunctionals X implies v + u in LinearFunctionals X )
assume A2: ( v in LinearFunctionals X & u in LinearFunctionals X ) ; :: thesis: v + u in LinearFunctionals X
reconsider f = v + u as Functional of X by FUNCT_2:66;
A3: f is additive

proof

let x, y be VECTOR of X; :: according to HAHNBAN:def 2 :: thesis: f . (x + y) = K55((f . x),(f . y))
reconsider vZ1 = v, uZ1 = u as Element of Funcs ( the carrier of X,REAL) ;
A4: uZ1 is linear-Functional of X by A2, Def7;
reconsider uZ11 = uZ1 as additive homogeneous Functional of X by A2, Def7;
reconsider x1 = x, y1 = y as Element of X ;
A5: vZ1 is linear-Functional of X by A2, Def7;
f . (x + y) = (uZ1 . (x + y)) + (vZ1 . (x + y)) by FUNCSDOM:1
.= ((uZ1 . x) + (uZ1 . y)) + (vZ1 . (x + y)) by A4, HAHNBAN:def 2
.= ((uZ1 . x) + (uZ1 . y)) + ((vZ1 . x) + (vZ1 . y)) by A5, HAHNBAN:def 2
.= (((uZ1 . x) + (vZ1 . x)) + (uZ1 . y)) + (vZ1 . y)
.= ((f . x) + (uZ1 . y)) + (vZ1 . y) by FUNCSDOM:1
.= (f . x) + ((uZ1 . y) + (vZ1 . y)) ;
hence f . (x + y) = (f . x) + (f . y) by FUNCSDOM:1; :: thesis: verum

end;

f is homogeneous

proof

let x be VECTOR of X; :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds f . (b₁ * x) = b₁ * (f . x)
let s be Real; :: thesis: f . (s * x) = s * (f . x)
reconsider v1 = v, u1 = u as Element of Funcs ( the carrier of X,REAL) ;
A6: ( u1 is linear-Functional of X & v1 is linear-Functional of X ) by A2, Def7;
f . (s * x) = (u1 . (s * x)) + (v1 . (s * x)) by FUNCSDOM:1
.= (s * (u1 . x)) + (v1 . (s * x)) by A6, HAHNBAN:def 3
.= (s * (u1 . x)) + (s * (v1 . x)) by A6, HAHNBAN:def 3
.= s * ((u1 . x) + (v1 . x)) ;
hence f . (s * x) = s * (f . x) by FUNCSDOM:1; :: thesis: verum

end;

hence v + u in LinearFunctionals X by A3, Def7; :: thesis: verum

end;

for a being Real
for v being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X holds
a * v in LinearFunctionals X

proof

let a be Real; :: thesis: for v being VECTOR of (RealVectSpace the carrier of X) st v in LinearFunctionals X holds
a * v in LinearFunctionals X
let v be VECTOR of (RealVectSpace the carrier of X); :: thesis: ( v in LinearFunctionals X implies a * v in LinearFunctionals X )
assume A8: v in LinearFunctionals X ; :: thesis: a * v in LinearFunctionals X
reconsider f = a * v as Functional of X by FUNCT_2:66;
A9: f is additive

proof

let x, y be VECTOR of X; :: according to HAHNBAN:def 2 :: thesis: f . (x + y) = K55((f . x),(f . y))
reconsider vZ1 = v as Element of Funcs ( the carrier of X,REAL) ;
A10: vZ1 is linear-Functional of X by Def7, A8;
f . (x + y) = a * (vZ1 . (x + y)) by FUNCSDOM:4
.= a * ((vZ1 . x) + (vZ1 . y)) by A10, HAHNBAN:def 2
.= (a * (vZ1 . x)) + (a * (vZ1 . y))
.= (f . x) + (a * (vZ1 . y)) by FUNCSDOM:4 ;
hence f . (x + y) = (f . x) + (f . y) by FUNCSDOM:4; :: thesis: verum

end;

f is homogeneous

proof

let x be VECTOR of X; :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds f . (b₁ * x) = b₁ * (f . x)
let s be Real; :: thesis: f . (s * x) = s * (f . x)
reconsider vZ1 = v as Element of Funcs ( the carrier of X,REAL) ;
A11: vZ1 is linear-Functional of X by Def7, A8;
f . (s * x) = a * (vZ1 . (s * x)) by FUNCSDOM:4
.= a * (s * (vZ1 . x)) by A11, HAHNBAN:def 3
.= s * (a * (vZ1 . x)) ;
hence f . (s * x) = s * (f . x) by FUNCSDOM:4; :: thesis: verum

end;

hence a * v in LinearFunctionals X by A9, Def7; :: thesis: verum

end;

hence LinearFunctionals X is linearly-closed by A1; :: thesis: verum