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;