let X be RealLinearSpace; :: thesis:
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:
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 ;
reconsider uZ11 = uZ1 as additive homogeneous Functional of X by ;
reconsider x1 = x, y1 = y as Element of X ;
A5: vZ1 is linear-Functional of X by ;
f . (x + y) = (uZ1 . (x + y)) + (vZ1 . (x + y)) by FUNCSDOM:1
.= ((uZ1 . x) + (uZ1 . y)) + (vZ1 . (x + y)) by
.= ((uZ1 . x) + (uZ1 . y)) + ((vZ1 . x) + (vZ1 . y)) by
.= (((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 b1 being object holds f . (b1 * x) = b1 * (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 ;
f . (s * x) = (u1 . (s * x)) + (v1 . (s * x)) by FUNCSDOM:1
.= (s * (u1 . x)) + (v1 . (s * x)) by
.= (s * (u1 . x)) + (s * (v1 . x)) by
.= 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 ; :: 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:
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 ;
f . (x + y) = a * (vZ1 . (x + y)) by FUNCSDOM:4
.= a * ((vZ1 . x) + (vZ1 . y)) by
.= (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 b1 being object holds f . (b1 * x) = b1 * (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 ;
f . (s * x) = a * (vZ1 . (s * x)) by FUNCSDOM:4
.= a * (s * (vZ1 . x)) by
.= s * (a * (vZ1 . x)) ;
hence f . (s * x) = s * (f . x) by FUNCSDOM:4; :: thesis: verum
end;
hence a * v in LinearFunctionals X by ; :: thesis: verum
end;
hence LinearFunctionals X is linearly-closed by A1; :: thesis: verum