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