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 ((0_. L),p) = 0_. L
let p be Polynomial of L; :: thesis: Subst ((0_. L),p) = 0_. L
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A1: Subst ((0_. L),p) = Sum F and
len F = len (0_. L) and
A2: for n being Element of NAT st n in dom F holds
F . n = ((0_. L) . (n -' 1)) * (p `^ (n -' 1)) by Def6;

now :: thesis: for n being Element of NAT st n in dom F holds
F . n = 0. (Polynom-Ring L)

let n be Element of NAT ; :: thesis: ( n in dom F implies F . n = 0. (Polynom-Ring L) )
assume n in dom F ; :: thesis: F . n = 0. (Polynom-Ring L)
hence F . n = ((0_. L) . (n -' 1)) * (p `^ (n -' 1)) by A2
.= (0. L) * (p `^ (n -' 1)) by FUNCOP_1:7
.= 0_. L by Th26
.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;
:: thesis: verum

end;

hence Subst ((0_. L),p) = 0. (Polynom-Ring L) by A1, POLYNOM3:1
.= 0_. L by POLYNOM3:def 10 ;
:: thesis: verum