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

.= (1 / 2) * (((g * f) . a) + ((g * f) . b)) by A3, A2 ; :: thesis: verum

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

.= (1 / 2) * (((g * f) . a) + ((g * f) . b)) by A3, A2 ; :: thesis: verum