let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL
for g being Function of (),REAL st f = g holds
( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )

let f be Function of X,REAL; :: thesis: for g being Function of (),REAL st f = g holds
( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )

let g be Function of (),REAL; :: thesis: ( f = g implies ( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) ) )
assume AS: f = g ; :: thesis: ( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )
set Y = RUSp2RNSp X;
hereby :: thesis: ( g is additive & g is homogeneous implies ( f is additive & f is homogeneous ) )
assume AS1: ( f is additive & f is homogeneous ) ; :: thesis: ( g is additive & g is homogeneous )
A1: g is additive
proof
let x, y be Point of (); :: according to HAHNBAN:def 2 :: thesis: g . (x + y) = K55((g . x),(g . y))
reconsider x1 = x, y1 = y as Point of X ;
thus g . (x + y) = f . (x1 + y1) by AS
.= (g . x) + (g . y) by ; :: thesis: verum
end;
g is homogeneous
proof
let x be Point of (); :: according to HAHNBAN:def 3 :: thesis: for b1 being object holds g . (b1 * x) = b1 * (g . x)
let r be Real; :: thesis: g . (r * x) = r * (g . x)
reconsider x1 = x as Point of X ;
thus g . (r * x) = f . (r * x1) by AS
.= r * (g . x) by ; :: thesis: verum
end;
hence ( g is additive & g is homogeneous ) by A1; :: thesis: verum
end;
assume AS2: ( g is additive & g is homogeneous ) ; :: thesis: ( f is additive & f is homogeneous )
A2: f is additive
proof
let x, y be Point of X; :: according to HAHNBAN:def 2 :: thesis: f . (x + y) = K55((f . x),(f . y))
reconsider x1 = x, y1 = y as Point of () ;
thus f . (x + y) = g . (x1 + y1) by AS
.= (f . x) + (f . y) by ; :: thesis: verum
end;
f is homogeneous
proof
let x be Point of X; :: according to HAHNBAN:def 3 :: thesis: for b1 being object holds f . (b1 * x) = b1 * (f . x)
let r be Real; :: thesis: f . (r * x) = r * (f . x)
reconsider x1 = x as Point of () ;
thus f . (r * x) = g . (r * x1) by AS
.= r * (f . x) by ; :: thesis: verum
end;
hence ( f is additive & f is homogeneous ) by A2; :: thesis: verum