let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L holds p *' (0_. L) = 0_. L
let p be Polynomial of L; :: thesis: p *' (0_. L) = 0_. L
now :: thesis: for i being Element of NAT holds (p *' (0_. L)) . i = (0_. L) . i
let i be Element of NAT ; :: thesis: (p *' (0_. L)) . i = (0_. L) . i
consider r being FinSequence of L such that
len r = i + 1 and
A1: (p *' (0_. L)) . i = Sum r and
A2: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by POLYNOM3:def 9;
now :: thesis: for k being Element of NAT st k in dom r holds
r . k = 0. L
let k be Element of NAT ; :: thesis: ( k in dom r implies r . k = 0. L )
assume k in dom r ; :: thesis: r . k = 0. L
hence r . k = (p . (k -' 1)) * ((0_. L) . ((i + 1) -' k)) by A2
.= (p . (k -' 1)) * (0. L) by FUNCOP_1:7
.= 0. L ;
:: thesis: verum
end;
hence (p *' (0_. L)) . i = 0. L by A1, POLYNOM3:1
.= (0_. L) . i by FUNCOP_1:7 ;
:: thesis: verum
end;
hence p *' (0_. L) = 0_. L by FUNCT_2:63; :: thesis: verum