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