theorem Th22: :: WALLIS01:25

for x being Function of REAL,REAL
for n being Nat
for a being Real st (@ (@ x)) . a > 0 holds
(@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n