let V be RealLinearSpace; :: thesis: for x being object holds
( x in the carrier of (V *') iff x is linear-Functional of V )
let x be object ; :: thesis: ( x in the carrier of (V *') iff x is linear-Functional of V )
consider X being VectSp of F_Real such that
AS1: ( X = RLSp2RVSp V & V *' = RVSp2RLSp (X *') ) by def2;
( x is linear-Functional of X iff x is linear-Functional of V )

proof

hereby :: thesis: ( x is linear-Functional of V implies x is linear-Functional of X )

assume A21: x is linear-Functional of X ; :: thesis: x is linear-Functional of V
then reconsider f = x as Functional of V by AS1;
reconsider g = x as linear-Functional of X by A21;
A1: f is additive

proof

let v, w be Element of V; :: according to HAHNBAN:def 2 :: thesis: f . (v + w) = K55((f . v),(f . w))
reconsider v1 = v, w1 = w as Element of X by AS1;
f . (v + w) = g . (v1 + w1) by AS1
.= (g . v1) + (g . w1) by VECTSP_1:def 20 ;
hence f . (v + w) = (f . v) + (f . w) ; :: thesis: verum

end;

f is homogeneous

proof

let v be VECTOR of V; :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds f . (b₁ * v) = b₁ * (f . v)
let r be Real; :: thesis: f . (r * v) = r * (f . v)
reconsider v1 = v as Element of X by AS1;
reconsider r1 = r as Scalar of by XREAL_0:def 1;
f . (r * v) = g . (r1 * v1) by AS1
.= r1 * (g . v1) by HAHNBAN1:def 8 ;
hence f . (r * v) = r * (f . v) ; :: thesis: verum

end;

hence x is linear-Functional of V by A1; :: thesis: verum

end;

assume A21: x is linear-Functional of V ; :: thesis: x is linear-Functional of X
then reconsider f = x as Functional of X by AS1;
reconsider g = x as linear-Functional of V by A21;
A1: f is additive

proof

let v, w be Element of X; :: according to VECTSP_1:def 19 :: thesis: f . (v + w) = (f . v) + (f . w)
reconsider v1 = v, w1 = w as VECTOR of V by AS1;
f . (v + w) = g . (v1 + w1) by AS1;
hence f . (v + w) = (f . v) + (f . w) by HAHNBAN:def 2; :: thesis: verum

end;

f is homogeneous

proof

let v be Element of X; :: according to HAHNBAN1:def 8 :: thesis: for b₁ being Element of the carrier of F_Real holds f . (b₁ * v) = b₁ * (f . v)
let r be Element of F_Real; :: thesis: f . (r * v) = r * (f . v)
reconsider v1 = v as Element of V by AS1;
reconsider r1 = r as Element of REAL ;
f . (r * v) = g . (r1 * v1) by AS1;
hence f . (r * v) = r * (f . v) by HAHNBAN:def 3; :: thesis: verum

end;

hence x is linear-Functional of X by A1; :: thesis: verum

end;

hence ( x in the carrier of (V *') iff x is linear-Functional of V ) by AS1, HAHNBAN1:def 10; :: thesis: verum