theorem Th23: :: WALLIS01:26

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