let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive 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 Def5;

per cases ( len F <> 0 or len F = 0 ) ;

suppose len F <> 0 ; :: thesis: Subst p,(0_. L) = <%(p . 0 )%>

then len F > 0 ;
then 0 + 1 <= len F by NAT_1:13;
then A4: 1 in dom F by FINSEQ_3:27;

now

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:27;
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:11;
n - 1 >= 0 by A7, XREAL_1:21;
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 8
.= (p . (n -' 1)) * ((0_. L) `^ (n -' 1)) by A3, A5
.= (p . (n -' 1)) * (0_. L) by A9, Th21
.= 0_. L by Th29
.= 0. (Polynom-Ring L) by POLYNOM3:def 12 ; :: thesis: verum

end;

hence Subst p,(0_. L) = F /. 1 by A1, A4, POLYNOM2:5
.= F . 1 by A4, PARTFUN1:def 8
.= (p . (1 -' 1)) * ((0_. L) `^ (1 -' 1)) by A3, A4
.= (p . (1 -' 1)) * ((0_. L) `^ 0 ) by XREAL_1:234
.= (p . 0 ) * ((0_. L) `^ 0 ) by XREAL_1:234
.= (p . 0 ) * (1_. L) by Th16
.= <%(p . 0 )%> by Th30 ;
:: thesis: verum

end;

suppose len F = 0 ; :: thesis: Subst p,(0_. L) = <%(p . 0 )%>

then A10: p = 0_. L by A2, POLYNOM4:8;
hence Subst p,(0_. L) = 0_. L by Th50
.= <%(0. L)%> by Th35
.= <%(p . 0 )%> by A10, FUNCOP_1:13 ;
:: thesis: verum

end;

end;