let E, F be RealNormSpace; :: thesis: for f being Function of E,F st f is bijective & f is midpoints-preserving holds

f /" is midpoints-preserving

let f be Function of E,F; :: thesis: ( f is bijective & f is midpoints-preserving implies f /" is midpoints-preserving )

assume that

A1: f is bijective and

A2: f is midpoints-preserving ; :: thesis: f /" is midpoints-preserving

set g = f /" ;

let a, b be Point of F; :: according to MAZURULM:def 3 :: thesis: (f /") . ((1 / 2) * (a + b)) = (1 / 2) * (((f /") . a) + ((f /") . b))

A3: (f /") * f = id E by A1, Lm3;

( f . ((f /") . a) = a & f . ((f /") . b) = b ) by A1, Lm2;

hence (f /") . ((1 / 2) * (a + b)) = (f /") . (f . ((1 / 2) * (((f /") . a) + ((f /") . b)))) by A2

.= ((f /") * f) . ((1 / 2) * (((f /") . a) + ((f /") . b))) by FUNCT_2:15

.= (1 / 2) * (((f /") . a) + ((f /") . b)) by A3 ;

:: thesis: verum

f /" is midpoints-preserving

let f be Function of E,F; :: thesis: ( f is bijective & f is midpoints-preserving implies f /" is midpoints-preserving )

assume that

A1: f is bijective and

A2: f is midpoints-preserving ; :: thesis: f /" is midpoints-preserving

set g = f /" ;

let a, b be Point of F; :: according to MAZURULM:def 3 :: thesis: (f /") . ((1 / 2) * (a + b)) = (1 / 2) * (((f /") . a) + ((f /") . b))

A3: (f /") * f = id E by A1, Lm3;

( f . ((f /") . a) = a & f . ((f /") . b) = b ) by A1, Lm2;

hence (f /") . ((1 / 2) * (a + b)) = (f /") . (f . ((1 / 2) * (((f /") . a) + ((f /") . b)))) by A2

.= ((f /") * f) . ((1 / 2) * (((f /") . a) + ((f /") . b))) by FUNCT_2:15

.= (1 / 2) * (((f /") . a) + ((f /") . b)) by A3 ;

:: thesis: verum