let k be Integer; :: thesis: 1 #Z k = 1

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

suppose k >= 0 ; :: thesis: 1 #Z k = 1

hence 1 #Z k = 1 |^ (abs k) by Def4
.= 1 by NEWTON:10 ;
:: thesis: verum

end;

suppose k < 0 ; :: thesis: 1 #Z k = 1

then 1 #Z k = (1 |^ (abs k)) " by Def4;
hence 1 #Z k = 1 by Lm4, NEWTON:10; :: thesis: verum

end;

end;