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