let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr ; :: thesis: for p being Polynomial of L holds Subst (p,(0_. L)) = <%(p . 0)%>
let p be Polynomial of L; :: thesis: Subst (p,(0_. L)) = <%(p . 0)%>
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A1: Subst (p,(0_. L)) = Sum F and
A2: len F = len p and
A3: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((0_. L) `^ (n -' 1)) by Def6;
per cases ( len F <> 0 or len F = 0 ) ;
suppose len F <> 0 ; :: thesis: Subst (p,(0_. L)) = <%(p . 0)%>
then 0 + 1 <= len F by NAT_1:13;
then A4: 1 in dom F by FINSEQ_3:25;
now :: thesis: for n being Element of NAT st n in dom F & n <> 1 holds
F /. n = 0. (Polynom-Ring L)
let n be Element of NAT ; :: thesis: ( n in dom F & n <> 1 implies F /. n = 0. (Polynom-Ring L) )
assume that
A5: n in dom F and
A6: n <> 1 ; :: thesis: F /. n = 0. (Polynom-Ring L)
n >= 1 by A5, FINSEQ_3:25;
then A7: n > 0 + 1 by A6, XXREAL_0:1;
then n >= 1 + 1 by NAT_1:13;
then A8: n - 2 >= (1 + 1) - 2 by XREAL_1:9;
n - 1 >= 0 by A7;
then A9: n -' 1 = (n - (1 + 1)) + 1 by XREAL_0:def 2
.= (n -' 2) + 1 by A8, XREAL_0:def 2 ;
thus F /. n = F . n by A5, PARTFUN1:def 6
.= (p . (n -' 1)) * ((0_. L) `^ (n -' 1)) by A3, A5
.= (p . (n -' 1)) * (0_. L) by A9, Th20
.= 0_. L by Th28
.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ; :: thesis: verum
end;
hence Subst (p,(0_. L)) = F /. 1 by A1, A4, POLYNOM2:3
.= F . 1 by A4, PARTFUN1:def 6
.= (p . (1 -' 1)) * ((0_. L) `^ (1 -' 1)) by A3, A4
.= (p . (1 -' 1)) * ((0_. L) `^ 0) by XREAL_1:232
.= (p . 0) * ((0_. L) `^ 0) by XREAL_1:232
.= (p . 0) * (1_. L) by Th15
.= <%(p . 0)%> by Th29 ;
:: thesis: verum
end;
suppose len F = 0 ; :: thesis: Subst (p,(0_. L)) = <%(p . 0)%>
then A10: p = 0_. L by A2, POLYNOM4:5;
hence Subst (p,(0_. L)) = 0_. L by Th49
.= <%(0. L)%> by Th34
.= <%(p . 0)%> by A10, FUNCOP_1:7 ;
:: thesis: verum
end;
end;