take [ the Polynomial of L, the non zero Polynomial of L] ; :: thesis: ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st [ the Polynomial of L, the non zero Polynomial of L] = [p1,p2]
thus ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st [ the Polynomial of L, the non zero Polynomial of L] = [p1,p2] ; :: thesis: verum