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
B: x is_a_common_root_of [(0_. L),(1_. L)] `1 ,[(0_. L),(1_. L)] `2 by root2;
x is_a_root_of [(0_. L),(1_. L)] `2 by B, root1;
then eval (([(0_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def 6;
hence contradiction by POLYNOM4:18; :: thesis: verum

end;

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