set z = [(0_. L),(1_. L)];
set p1 = [(0_. L),(1_. L)] `1 ;
set p2 = [(0_. L),(1_. L)] `2 ;

now :: thesis: not [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 have_a_common_root

assume [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 have_a_common_root ; :: thesis: contradiction
then consider x being Element of L such that
A1: x is_a_common_root_of [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 ;
x is_a_root_of [(0_. L),(1_. L)] `2 by A1;
then eval (([(0_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def 7;
hence contradiction by POLYNOM4:18; :: thesis: verum

end;

then A2: [(0_. L),(1_. L)] is irreducible ;
A3: len (1_. L) = 1 by POLYNOM4:4;
(len (1_. L)) -' 1 = 1 - 1 by A3, XREAL_0:def 2;
then LC (1_. L) = 1. L by POLYNOM3:30;
then [(0_. L),(1_. L)] `2 is normalized ;
hence 0._ L is normalized by A2; :: thesis: verum