let L be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for p being sequence of L holds (0_. L) *' p = 0_. L
let p be sequence of L; :: thesis: (0_. L) *' p = 0_. L

now :: thesis: for i being Element of NAT holds ((0_. L) *' p) . i = (0_. L) . i

let i be Element of NAT ; :: thesis: ((0_. L) *' p) . i = (0_. L) . i
consider r being FinSequence of the carrier of L such that
len r = i + 1 and
A1: ((0_. L) *' p) . i = Sum r and
A2: for k being Element of NAT st k in dom r holds
r . k = ((0_. L) . (k -' 1)) * (p . ((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 = ((0_. L) . (k -' 1)) * (p . ((i + 1) -' k)) by A2
.= (0. L) * (p . ((i + 1) -' k)) by FUNCOP_1:7
.= 0. L ;
:: thesis: verum

end;

hence ((0_. L) *' p) . i = 0. L by A1, POLYNOM3:1
.= (0_. L) . i by FUNCOP_1:7 ;
:: thesis: verum

end;

hence (0_. L) *' p = 0_. L by FUNCT_2:63; :: thesis: verum