let X be RealUnitarySpace; :: thesis:
let f be Function of X,REAL; :: thesis:
let g be Function of (RUSp2RNSp X),REAL; :: thesis:
assume AS: f = g ; :: thesis:
set Y = RUSp2RNSp X;

hereby :: thesis:

assume AS1: ( f is additive & f is homogeneous ) ; :: thesis:
A1: g is additive

proof

let x, y be Point of (RUSp2RNSp X); :: according to HAHNBAN:def 2 :: thesis:
reconsider x1 = x, y1 = y as Point of X ;
thus g . (x + y) = f . (x1 + y1) by AS
.= (g . x) + (g . y) by AS, AS1, HAHNBAN:def 2 ; :: thesis:

end;

g is homogeneous

proof

let x be Point of (RUSp2RNSp X); :: according to HAHNBAN:def 3 :: thesis:
let r be Real; :: thesis:
reconsider x1 = x as Point of X ;
thus g . (r * x) = f . (r * x1) by AS
.= r * (g . x) by AS, AS1, HAHNBAN:def 3 ; :: thesis:

end;

hence ( g is additive & g is homogeneous ) by A1; :: thesis:

end;

assume AS2: ( g is additive & g is homogeneous ) ; :: thesis:
A2: f is additive

proof

let x, y be Point of X; :: according to HAHNBAN:def 2 :: thesis:
reconsider x1 = x, y1 = y as Point of (RUSp2RNSp X) ;
thus f . (x + y) = g . (x1 + y1) by AS
.= (f . x) + (f . y) by AS, AS2, HAHNBAN:def 2 ; :: thesis:

end;

f is homogeneous

proof

let x be Point of X; :: according to HAHNBAN:def 3 :: thesis:
let r be Real; :: thesis:
reconsider x1 = x as Point of (RUSp2RNSp X) ;
thus f . (r * x) = g . (r * x1) by AS
.= r * (f . x) by AS, AS2, HAHNBAN:def 3 ; :: thesis:

end;

hence ( f is additive & f is homogeneous ) by A2; :: thesis: