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