consider p1 being Polynomial of L such that
A3: ex p2 being non zero Polynomial of L st z = [p1,p2] by Def8;
consider p2 being non zero Polynomial of L such that
A4: z = [p1,p2] by A3;
thus z `2 is non zero Polynomial of L by A4; :: thesis: verum