theorem :: FLEXARY1:25

for f being real-valued Function
for g being Function holds (2 |^ f) * g = 2 |^ (f * g)