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 )

( 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

then reconsider f = x as Functional of X by AS1;

reconsider g = x as linear-Functional of V by A21;

A1: f is additive

end;

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

assume A21:
x is linear-Functional of V
; :: thesis: x is linear-Functional of Xassume 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

end;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

f is homogeneous
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;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

proof

hence
x is linear-Functional of V
by A1; :: thesis: verum
let v be VECTOR of V; :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds f . (b_{1} * v) = b_{1} * (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;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

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

f is homogeneous
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;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

proof

hence
x is linear-Functional of X
by A1; :: thesis: verum
let v be Element of X; :: according to HAHNBAN1:def 8 :: thesis: for b_{1} being Element of the carrier of F_Real holds f . (b_{1} * v) = b_{1} * (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;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