let X be RealLinearSpace; :: thesis: the carrier of X --> 0 is linear-Functional of X
set f = the carrier of X --> 0;
reconsider f = the carrier of X --> 0 as Functional of X by FUNCOP_1:45, XREAL_0:def 1;
A1: 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))
thus f . (x + y) = (f . x) + (f . y) ; :: 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 r be Real; :: thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = r * (f . x) ; :: thesis: verum

end;

hence the carrier of X --> 0 is linear-Functional of X by A1; :: thesis: verum