ex x1 being State of s ex x2 being State of t st x = [x1,x2] by Th47;
hence x `1 is State of s by MCART_1:def 1; :: thesis: verum