set p1 = the non zero Polynomial of L;
set p2 = the non zero Polynomial of L;
take [ the non zero Polynomial of L, the non zero Polynomial of L] ; :: thesis: not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero
H: the non zero Polynomial of L = [ the non zero Polynomial of L, the non zero Polynomial of L] `1 ;
the non zero Polynomial of L <> 0_. L ;
hence not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero by H, defzerrat; :: thesis: verum