let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL
for g being Function of (RUSp2RNSp X),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 (RUSp2RNSp X),REAL st f = g holds
( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )
let g be Function of (RUSp2RNSp X),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 (RUSp2RNSp X); :: 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 AS, AS1, HAHNBAN:def 2 ; :: thesis: verum

end;

g is homogeneous

proof

let x be Point of (RUSp2RNSp X); :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds g . (b₁ * x) = b₁ * (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 AS, AS1, HAHNBAN:def 3 ; :: 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 (RUSp2RNSp X) ;
thus f . (x + y) = g . (x1 + y1) by AS
.= (f . x) + (f . y) by AS, AS2, HAHNBAN:def 2 ; :: thesis: verum

end;

f is homogeneous

proof

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

end;

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