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

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

f is homogeneous
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;thus f . (x + y) = (f . x) + (f . y) ; :: thesis: verum

proof

hence
the carrier of X --> 0 is linear-Functional of X
by A1; :: thesis: verum
let x be VECTOR of X; :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds f . (b_{1} * x) = b_{1} * (f . x)

let r be Real; :: thesis: f . (r * x) = r * (f . x)

thus f . (r * x) = r * (f . x) ; :: thesis: verum

end;let r be Real; :: thesis: f . (r * x) = r * (f . x)

thus f . (r * x) = r * (f . x) ; :: thesis: verum