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