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;

A2: f is additive

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 AS2:
( g is additive & g is homogeneous )
; :: thesis: ( 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

end;A1: g is additive

proof

g is homogeneous
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;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

proof

hence
( g is additive & g is homogeneous )
by A1; :: thesis: verum
let x be Point of (RUSp2RNSp X); :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds g . (b_{1} * x) = b_{1} * (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;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

A2: f is additive

proof

f is homogeneous
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;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

proof

hence
( f is additive & f is homogeneous )
by A2; :: thesis: verum
let x be Point of X; :: according to HAHNBAN:def 3 :: thesis: for b_{1} being object holds f . (b_{1} * x) = b_{1} * (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;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