reconsider
mm
=
r
as
Element
of
INT
by
INT_1:def 2
;
take
r
;
:: thesis:
ex
f
being
FinSequence
of
INT
st
(
f
=
x
`3_3
&
r
=
f
/.
1 )
take
<*
mm
*>
;
:: thesis:
(
<*
mm
*>
=
x
`3_3
&
r
=
<*
mm
*>
/.
1 )
thus
(
<*
mm
*>
=
x
`3_3
&
r
=
<*
mm
*>
/.
1 )
by
A1
,
FINSEQ_4:16
;
:: thesis:
verum