theorem :: FUZIMPL2:4

for x being Element of [.0,1.]
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)