reconsider f = BidualFunc X as Function of X,(DualSp (DualSp X)) ;
A0: f is additive

proof

let x, y be Point of X; :: according to VECTSP_1:def 19 :: thesis: f . (x + y) = (f . x) + (f . y)
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

proof

let g be Point of (DualSp X); :: thesis: (f . (x + y)) . g = ((f . x) + (f . y)) . g
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: verum

end;

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

end;

f is homogeneous

proof

let x be Point of X; :: according to LOPBAN_1:def 5 :: thesis: for b₁ being object holds f . (b₁ * x) = b₁ * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
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

proof

let g be Point of (DualSp X); :: thesis: (f . (r * x)) . g = (r * (f . x)) . g
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: verum

end;

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

end;

hence ( BidualFunc X is additive & BidualFunc X is homogeneous ) by A0; :: thesis: verum