consider
i
being
Nat
such that
i
<=
2
|^
n
and
A1
:
x
=
i
/
(
2
|^
n
)
by
Def1
;
take
i
;
:: thesis:
x
=
i
/
(
2
|^
n
)
thus
x
=
i
/
(
2
|^
n
)
by
A1
;
:: thesis:
verum