theorem Th34: :: AMI_8:34

for n being Nat holds powerSCMFunction . (((dl. 0),(dl. 1),(dl. 2)) --> (1,n,1)) = (dl. 2) .--> (n !)