per cases ( i < 0 or i >= 0 ) ;

suppose i < 0 ; :: thesis: a #Z i is rational

then a #Z i = (a |^ |.i.|) " by PREPOWER:def 3;
hence a #Z i is rational ; :: thesis: verum

end;

suppose i >= 0 ; :: thesis: a #Z i is rational

then a #Z i = a |^ |.i.| by PREPOWER:def 3;
hence a #Z i is rational ; :: thesis: verum

end;

end;