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