theorem :: SIN_COS2:29

for p being Real
for n being Nat holds ((cosh . p) + (sinh . p)) |^ n = (cosh . (n * p)) + (sinh . (n * p))