let f be real-valued Function; :: thesis: for g being Function holds (2 |^ f) * g = 2 |^ (f * g)
let g be Function; :: thesis: (2 |^ f) * g = 2 |^ (f * g)
set 2f = 2 |^ f;
set fg = f * g;
A1: ( dom (2 |^ f) = dom f & dom (2 |^ (f * g)) = dom (f * g) ) by Def4;
A2: dom ((2 |^ f) * g) c= dom (2 |^ (f * g))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((2 |^ f) * g) or x in dom (2 |^ (f * g)) )
assume x in dom ((2 |^ f) * g) ; :: thesis: x in dom (2 |^ (f * g))
then ( x in dom g & g . x in dom (2 |^ f) ) by FUNCT_1:11;
hence x in dom (2 |^ (f * g)) by A1, FUNCT_1:11; :: thesis: verum

end;

dom (2 |^ (f * g)) c= dom ((2 |^ f) * g)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (2 |^ (f * g)) or x in dom ((2 |^ f) * g) )
assume x in dom (2 |^ (f * g)) ; :: thesis: x in dom ((2 |^ f) * g)
then ( x in dom g & g . x in dom f ) by A1, FUNCT_1:11;
hence x in dom ((2 |^ f) * g) by A1, FUNCT_1:11; :: thesis: verum

end;

then A3: dom (2 |^ (f * g)) = dom ((2 |^ f) * g) by A2;
for x being object st x in dom (2 |^ (f * g)) holds
((2 |^ f) * g) . x = (2 |^ (f * g)) . x

proof

let x be object ; :: thesis: ( x in dom (2 |^ (f * g)) implies ((2 |^ f) * g) . x = (2 |^ (f * g)) . x )
assume A4: x in dom (2 |^ (f * g)) ; :: thesis: ((2 |^ f) * g) . x = (2 |^ (f * g)) . x
then ( x in dom g & g . x in dom f ) by A1, FUNCT_1:11;
then ( ((2 |^ f) * g) . x = (2 |^ f) . (g . x) & (2 |^ f) . (g . x) = 2 to_power (f . (g . x)) & f . (g . x) = (f * g) . x ) by Def4, FUNCT_1:13;
hence ((2 |^ f) * g) . x = (2 |^ (f * g)) . x by A4, A1, Def4; :: thesis: verum

end;

hence (2 |^ f) * g = 2 |^ (f * g) by A3; :: thesis: verum