((a,b) In_Power ((n + 1) - 1)) null n is n + 1 -element ;
hence (a,b) In_Power n is n + 1 -element ; :: thesis: verum