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