let
a
be
Real
;
:: thesis:
for
k
being
Integer
holds
(
1
/
a
)
#Z
k
=
1
/
(
a
#Z
k
)
let
k
be
Integer
;
:: thesis:
(
1
/
a
)
#Z
k
=
1
/
(
a
#Z
k
)
per
cases
(
k
>=
0
or
k
<
0
)
;
suppose
A1
:
k
>=
0
;
:: thesis:
(
1
/
a
)
#Z
k
=
1
/
(
a
#Z
k
)
hence
(
1
/
a
)
#Z
k
=
(
1
/
a
)
|^
|.
k
.|
by
Def3
.= 1
/
(
a
|^
|.
k
.|
)
by
Th7
.= 1
/
(
a
#Z
k
)
by
A1
,
Def3
;
:: thesis:
verum
end;
suppose
A2
:
k
<
0
;
:: thesis:
(
1
/
a
)
#Z
k
=
1
/
(
a
#Z
k
)
hence
(
1
/
a
)
#Z
k
=
(
(
1
/
a
)
|^
|.
k
.|
)
"
by
Def3
.=
(
1
/
(
a
|^
|.
k
.|
)
)
"
by
Th7
.=
(
(
a
|^
|.
k
.|
)
"
)
"
.=
(
a
#Z
k
)
"
by
A2
,
Def3
.= 1
/
(
a
#Z
k
)
;
:: thesis:
verum
end;
end;