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

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