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

let p be sequence of L; :: thesis: p *' (0_. L) = 0_. L

let p be sequence 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
; :: thesis: verumlet i be Element of NAT ; :: thesis: (p *' (0_. L)) . i = (0_. L) . i

consider r being FinSequence of the carrier 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 Def9;

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

:: thesis: verum

end;consider r being FinSequence of the carrier 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 Def9;

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, Th1
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