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 |^ |.k.| by Def3
.= 1 ;
:: thesis: verum

end;

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

1 #Z k = (1 |^ |.k.|) " by Def3;
hence 1 #Z k = 1 ; :: thesis: verum

end;

end;