set p = 1_. L;

now :: thesis:

per cases ;

suppose A1: 0. L = 1. L ; :: thesis:

A2: dom (1_. L) = NAT by FUNCT_2:def 1
.= dom (0_. L) by FUNCT_2:def 1 ;

now :: thesis:

let x be object ; :: thesis:
assume x in dom (1_. L) ; :: thesis:
then reconsider xx = x as Element of NAT ;
A3: (0_. L) . xx = 0. L by FUNCOP_1:7;
( xx = 0 or xx <> 0 ) ;
hence (1_. L) . x = (0_. L) . x by A1, A3, POLYNOM3:30; :: thesis:

end;

hence 1_. L is constant by A2, FUNCT_1:2; :: thesis:

end;

suppose A4: 0. L <> 1. L ; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume A5: i >= 1 ; :: thesis:
A6: i in NAT by ORDINAL1:def 12;
thus (1_. L) . i = (0_. L) . i by A5, FUNCT_7:32
.= 0. L by A6, FUNCOP_1:7 ; :: thesis:

end;

then A7: 1 is_at_least_length_of 1_. L by ALGSEQ_1:def 2;

now :: thesis:

let m be Nat; :: thesis:
assume A8: m is_at_least_length_of 1_. L ; :: thesis:

now :: thesis:

assume m < 1 ; :: thesis:
then m < 1 + 0 ;
then m <= 0 by NAT_1:13;
then A9: (1_. L) . 0 = 0. L by A8, ALGSEQ_1:def 2;
dom (0_. L) = NAT by FUNCOP_1:13;
hence contradiction by A4, A9, FUNCT_7:31; :: thesis:

end;

hence 1 <= m ; :: thesis:

end;

then len (1_. L) = 1 by A7, ALGSEQ_1:def 3;
then deg (1_. L) = 0 ;
hence 1_. L is constant ; :: thesis:

end;

end;

end;

hence 1_. L is constant ; :: thesis: