let L be Ring; :: thesis: for p being Element of the carrier of (Polynom-Ring L) holds
( p is constant iff ex a being Element of L st p = a | L )
let p be Element of the carrier of (Polynom-Ring L); :: thesis: ( p is constant iff ex a being Element of L st p = a | L )
reconsider g = p as Polynomial of L ;

now :: thesis: ( p is constant implies ex a being Element of L st p = a | L )

assume p is constant ; :: thesis: ex a being Element of L st p = a | L
then AS: ((len p) - 1) + 1 <= 0 + 1 by XREAL_1:6;

per cases ( len p = 0 or len p = 1 ) by AS, NAT_1:25;

suppose len p = 0 ; :: thesis: ex a being Element of L st p = a | L

then p = 0_. L by POLYNOM4:5
.= (0. L) | L by T6 ;
hence ex a being Element of L st p = a | L ; :: thesis: verum

end;

suppose AS: len p = 1 ; :: thesis: ex a being Element of L st p = a | L

set q = (p . 0) | L;

now :: thesis: for x being object st x in NAT holds
((p . 0) | L) . x = p . x

let x be object ; :: thesis: ( x in NAT implies ((p . 0) | L) . b₁ = p . b₁ )
assume x in NAT ; :: thesis: ((p . 0) | L) . b₁ = p . b₁
then reconsider i = x as Element of NAT ;

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: ((p . 0) | L) . b₁ = p . b₁

hence ((p . 0) | L) . x = p . x by Th28; :: thesis: verum

end;

suppose B: i <> 0 ; :: thesis: p . b₁ = ((p . 0) | L) . b₁

then i + 1 > 0 + 1 by XREAL_1:6;
then i >= len p by AS, NAT_1:13;
hence p . x = 0. L by ALGSEQ_1:8
.= ((p . 0) | L) . x by B, Th28 ;
:: thesis: verum

end;

end;

end;

hence ex a being Element of L st p = a | L by FUNCT_2:12; :: thesis: verum

end;

end;

end;

hence ( p is constant iff ex a being Element of L st p = a | L ) by RATFUNC1:def 2; :: thesis: verum