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) . b1 = p . b1 )
assume x in NAT ; :: thesis: ((p . 0) | L) . b1 = p . b1
then reconsider i = x as Element of NAT ;
per cases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; :: thesis: ((p . 0) | L) . b1 = p . b1
hence ((p . 0) | L) . x = p . x by Th28; :: thesis: verum
end;
suppose B: i <> 0 ; :: thesis: p . b1 = ((p . 0) | L) . b1
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