for k being Nat holds EXP k is multiplicative