let k be Nat; :: thesis: eta (k,k) = k !
eta (k,k) = (k !) / 1 by NEWTON:12, XREAL_1:232
.= k ! ;
hence eta (k,k) = k ! ; :: thesis: verum