consider
x1
being
State
of
s
,
x2
being
State
of
t
such that
A1
:
x
=
[
x1
,
x2
]
by
Th42
;
thus
x
`1
is
State
of
s
by
A1
;
:: thesis:
verum