let X be RealNormSpace; :: thesis: for x being object holds
( x is additive homogeneous Function of X,REAL iff x is additive homogeneous Function of X,RNS_Real )
let x be object ; :: thesis: ( x is additive homogeneous Function of X,REAL iff x is additive homogeneous Function of X,RNS_Real )

hereby :: thesis: ( x is additive homogeneous Function of X,RNS_Real implies x is additive homogeneous Function of X,REAL )

assume A1: x is additive homogeneous Function of X,REAL ; :: thesis: x is additive homogeneous Function of X,RNS_Real
then reconsider f = x as linear-Functional of X ;
reconsider g = x as Function of X,RNS_Real by A1;
A2: for v, w being Element of X holds g . (v + w) = (g . v) + (g . w)

proof

let v, w be Element of X; :: thesis: g . (v + w) = (g . v) + (g . w)
thus g . (v + w) = (f . v) + (f . w) by HAHNBAN:def 2
.= (g . v) + (g . w) by BINOP_2:def 9 ; :: thesis: verum

end;

for v being VECTOR of X
for r being Real holds g . (r * v) = r * (g . v)

proof

let v be VECTOR of X; :: thesis: for r being Real holds g . (r * v) = r * (g . v)
let r be Real; :: thesis: g . (r * v) = r * (g . v)
thus g . (r * v) = r * (f . v) by HAHNBAN:def 3
.= r * (g . v) by BINOP_2:def 11 ; :: thesis: verum

end;

then ( g is additive & g is homogeneous ) by LOPBAN_1:def 5, A2;
hence x is additive homogeneous Function of X,RNS_Real ; :: thesis: verum

end;

assume B1: x is additive homogeneous Function of X,RNS_Real ; :: thesis: x is additive homogeneous Function of X,REAL
then reconsider g = x as additive homogeneous Function of X,RNS_Real ;
reconsider f = x as Function of X,REAL by B1;
B2: for v, w being Element of X holds f . (v + w) = (f . v) + (f . w)

proof

let v, w be Element of X; :: thesis: f . (v + w) = (f . v) + (f . w)
thus f . (v + w) = (g . v) + (g . w) by VECTSP_1:def 20
.= (f . v) + (f . w) by BINOP_2:def 9 ; :: thesis: verum

end;

for v being VECTOR of X
for r being Real holds f . (r * v) = r * (f . v)

proof

let v be VECTOR of X; :: thesis: for r being Real holds f . (r * v) = r * (f . v)
let r be Real; :: thesis: f . (r * v) = r * (f . v)
thus f . (r * v) = r * (g . v) by LOPBAN_1:def 5
.= r * (f . v) by BINOP_2:def 11 ; :: thesis: verum

end;

hence x is additive homogeneous Function of X,REAL by B2, HAHNBAN:def 2, HAHNBAN:def 3; :: thesis: verum