theorem Th28: :: FLEXARY1:28

for k, n being Nat
for f being natural-valued Function st n > 1 holds
Coim ((n |^ f),(n |^ k)) = Coim (f,k)