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