let V be RealLinearSpace; :: thesis: for f, h being VECTOR of (V *')

for a being Real holds

( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

let f, h be VECTOR of (V *'); :: thesis: for a being Real holds

( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

let a be Real; :: thesis: ( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

reconsider a1 = a as Element of F_Real by XREAL_0:def 1;

consider Y being VectSp of F_Real such that

AS1: ( Y = RLSp2RVSp V & V *' = RVSp2RLSp (Y *') ) by def2;

reconsider f1 = f, h1 = h as linear-Functional of Y by AS1, HAHNBAN1:def 10;

then for x being Element of Y holds h1 . x = a1 * (f1 . x) by AS1;

then h1 = a1 * f1 by HAHNBAN1:def 6;

hence h = a * f by AS1, HAHNBAN1:def 10; :: thesis: verum

for a being Real holds

( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

let f, h be VECTOR of (V *'); :: thesis: for a being Real holds

( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

let a be Real; :: thesis: ( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )

reconsider a1 = a as Element of F_Real by XREAL_0:def 1;

consider Y being VectSp of F_Real such that

AS1: ( Y = RLSp2RVSp V & V *' = RVSp2RLSp (Y *') ) by def2;

reconsider f1 = f, h1 = h as linear-Functional of Y by AS1, HAHNBAN1:def 10;

hereby :: thesis: ( ( for x being VECTOR of V holds h . x = a * (f . x) ) implies h = a * f )
end;

assume
for x being Element of V holds h . x = a * (f . x)
; :: thesis: h = a * fthen for x being Element of Y holds h1 . x = a1 * (f1 . x) by AS1;

then h1 = a1 * f1 by HAHNBAN1:def 6;

hence h = a * f by AS1, HAHNBAN1:def 10; :: thesis: verum