set p = 1_. L;

now :: thesis: 1_. L is constant

per cases ( 0. L = 1. L or 0. L <> 1. L ) ;

suppose A1: 0. L = 1. L ; :: thesis: 1_. L is constant

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

now :: thesis: for x being object st x in dom (1_. L) holds
(1_. L) . x = (0_. L) . x

let x be object ; :: thesis: ( x in dom (1_. L) implies (1_. L) . x = (0_. L) . x )
assume x in dom (1_. L) ; :: thesis: (1_. L) . x = (0_. L) . x
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: verum

end;

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

end;

suppose A4: 0. L <> 1. L ; :: thesis: 1_. L is constant

now :: thesis: for i being Nat st i >= 1 holds
(1_. L) . i = 0. L

let i be Nat; :: thesis: ( i >= 1 implies (1_. L) . i = 0. L )
assume A5: i >= 1 ; :: thesis: (1_. L) . i = 0. L
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: verum

end;

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

now :: thesis: for m being Nat st m is_at_least_length_of 1_. L holds
1 <= m

let m be Nat; :: thesis: ( m is_at_least_length_of 1_. L implies 1 <= m )
assume A8: m is_at_least_length_of 1_. L ; :: thesis: 1 <= m

now :: thesis: not m < 1

assume m < 1 ; :: thesis: contradiction
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: verum

end;

hence 1 <= m ; :: thesis: verum

end;

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

end;

end;

end;

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