theorem Th35: :: NAT_5:35

for k being Nat holds EXP k is multiplicative