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

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

hence
p *' (0_. L) = 0_. L
by FUNCT_2:63; :: thesis: verumlet 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;

.= (0_. L) . i by FUNCOP_1:7 ;

:: thesis: verum

end;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

hence (p *' (0_. L)) . i =
0. L
by A1, POLYNOM3:1
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;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

.= (0_. L) . i by FUNCOP_1:7 ;

:: thesis: verum