let E, F, G be RealNormSpace; :: thesis: for f being Function of E,F
for g being Function of F,G st f is midpoints-preserving & g is midpoints-preserving holds
g * f is midpoints-preserving
let f be Function of E,F; :: thesis: for g being Function of F,G st f is midpoints-preserving & g is midpoints-preserving holds
g * f is midpoints-preserving
let g be Function of F,G; :: thesis: ( f is midpoints-preserving & g is midpoints-preserving implies g * f is midpoints-preserving )
assume that
A1: f is midpoints-preserving and
A2: g is midpoints-preserving ; :: thesis: g * f is midpoints-preserving
set h = g * f;
let a be Point of E; :: according to MAZURULM:def 3 :: thesis: for b being Point of E holds (g * f) . ((1 / 2) * (a + b)) = (1 / 2) * (((g * f) . a) + ((g * f) . b))
let b be Point of E; :: thesis: (g * f) . ((1 / 2) * (a + b)) = (1 / 2) * (((g * f) . a) + ((g * f) . b))
A3: ( (g * f) . a = g . (f . a) & (g * f) . b = g . (f . b) ) by FUNCT_2:15;
thus (g * f) . ((1 / 2) * (a + b)) = g . (f . ((1 / 2) * (a + b))) by FUNCT_2:15
.= g . ((1 / 2) * ((f . a) + (f . b))) by A1, Def3
.= (1 / 2) * (((g * f) . a) + ((g * f) . b)) by A3, A2, Def3 ; :: thesis: verum