let x be Element of [.0,1.]; :: thesis: for u being Real st u in ].0,1.] holds
((#R x) + (AffineMap ((- x),(x - 1)))) . u = (((u to_power x) - 1) + x) - (x * u)

set f1 = #R x;
set f2 = AffineMap ((- x),(x - 1));
reconsider Y = ].0,1.[ as open Subset of REAL ;
set f = (#R x) + (AffineMap ((- x),(x - 1)));
set A = right_open_halfline 0;
BX: dom ((#R x) + (AffineMap ((- x),(x - 1)))) = (dom (#R x)) /\ (dom (AffineMap ((- x),(x - 1)))) by VALUED_1:def 1
.= /\ (dom (AffineMap ((- x),(x - 1)))) by TAYLOR_1:def 4
.= /\ REAL by FUNCT_2:def 1
.= right_open_halfline 0 by XBOOLE_1:28 ;
let u be Real; :: thesis: ( u in ].0,1.] implies ((#R x) + (AffineMap ((- x),(x - 1)))) . u = (((u to_power x) - 1) + x) - (x * u) )
assume S1: u in ].0,1.] ; :: thesis: ((#R x) + (AffineMap ((- x),(x - 1)))) . u = (((u to_power x) - 1) + x) - (x * u)
then ZE: u > 0 by XXREAL_1:2;
1 < +infty by ;
then h0: ].0,1.] c= by XXREAL_1:49;
then ((#R x) + (AffineMap ((- x),(x - 1)))) . u = ((#R x) . u) + ((AffineMap ((- x),(x - 1))) . u) by
.= (u #R x) + ((AffineMap ((- x),(x - 1))) . u) by
.= (u to_power x) + ((AffineMap ((- x),(x - 1))) . u) by
.= (u to_power x) + (((- x) * u) + (x - 1)) by FCONT_1:def 4
.= (u to_power x) + (((- (x * u)) + x) - 1) ;
hence ((#R x) + (AffineMap ((- x),(x - 1)))) . u = (((u to_power x) - 1) + x) - (x * u) ; :: thesis: verum