take n |^ 1 ; :: thesis: n |^ 1 is n -power
thus n |^ 1 is n -power ; :: thesis: verum