consider p1 being Polynomial of L such that
H: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf;
consider p2 being non zero Polynomial of L such that
H1: z = [p1,p2] by H;
thus z `1 is Polynomial of L by H1, XTUPLE_0:def 2; :: thesis: verum