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