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
.= (right_open_halfline 0) /\ (dom (AffineMap ((- x),(x - 1)))) by TAYLOR_1:def 4
.= (right_open_halfline 0) /\ 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 XXREAL_0:9, XREAL_0:def 1;
then h0: ].0,1.] c= ].0,+infty.[ by XXREAL_1:49;
then ((#R x) + (AffineMap ((- x),(x - 1)))) . u = ((#R x) . u) + ((AffineMap ((- x),(x - 1))) . u) by S1, BX, VALUED_1:def 1
.= (u #R x) + ((AffineMap ((- x),(x - 1))) . u) by TAYLOR_1:def 4, h0, S1
.= (u to_power x) + ((AffineMap ((- x),(x - 1))) . u) by ZE, POWER:def 2
.= (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