set p = 1_. L;

now :: thesis: 1_. L is constant

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

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

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

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

let x be set ; :: 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 ;
B: (0_. L) . xx = 0. L by FUNCOP_1:7;
( xx = 0 or xx <> 0 ) ;
hence (1_. L) . x = (0_. L) . x by I, B, POLYNOM3:30; :: thesis: verum

end;

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

end;

suppose I: 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 AS: i >= 1 ; :: thesis: (1_. L) . i = 0. L
B: i in NAT by ORDINAL1:def 12;
thus (1_. L) . i = (0_. L) . i by AS, FUNCT_7:32
.= 0. L by B, FUNCOP_1:7 ; :: thesis: verum

end;

then D: 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 AS: 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 E: (1_. L) . 0 = 0. L by AS, ALGSEQ_1:def 2;
dom (0_. L) = NAT by FUNCOP_1:13;
hence contradiction by I, E, FUNCT_7:31; :: thesis: verum

end;

hence 1 <= m ; :: thesis: verum

end;

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

end;

end;

end;

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