let x, y be Point of X; :: according to VECTSP_1:def 19 :: thesis:
A1: ( f . (x + y) is Function of the carrier of (DualSp X),REAL & (f . x) + (f . y) is Function of the carrier of (DualSp X),REAL ) by DUALSP01:def 10;
for g being Point of (DualSp X) holds (f . (x + y)) . g = ((f . x) + (f . y)) . g

let g be Point of (DualSp X); :: thesis:
reconsider g1 = g as Lipschitzian linear-Functional of X by DUALSP01:def 10;
thus (f . (x + y)) . g = (BiDual (x + y)) . g by Def2
.= g . (x + y) by Def1
.= (g1 . x) + (g1 . y) by HAHNBAN:def 2
.= ((BiDual x) . g) + (g . y) by Def1
.= ((BiDual x) . g) + ((BiDual y) . g) by Def1
.= ((f . x) . g) + ((BiDual y) . g) by Def2
.= ((f . x) . g) + ((f . y) . g) by Def2
.= ((f . x) + (f . y)) . g by DUALSP01:29 ; :: thesis:

end;

hence f . (x + y) = (f . x) + (f . y) by A1, FUNCT_2:def 8; :: thesis:

end;

let x be Point of X; :: according to LOPBAN_1:def 5 :: thesis:
let r be Real; :: thesis:
A3: ( f . (r * x) is Function of the carrier of (DualSp X),REAL & r * (f . x) is Function of the carrier of (DualSp X),REAL ) by DUALSP01:def 10;
for g being Point of (DualSp X) holds (f . (r * x)) . g = (r * (f . x)) . g

let g be Point of (DualSp X); :: thesis:
reconsider g1 = g as Lipschitzian linear-Functional of X by DUALSP01:def 10;
thus (f . (r * x)) . g = (BiDual (r * x)) . g by Def2
.= g . (r * x) by Def1
.= r * (g1 . x) by HAHNBAN:def 3
.= r * ((BiDual x) . g) by Def1
.= r * ((f . x) . g) by Def2
.= (r * (f . x)) . g by DUALSP01:30 ; :: thesis:

end;

hence f . (r * x) = r * (f . x) by A3, FUNCT_2:def 8; :: thesis:

end;