let L be non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr ; :: thesis: for a being Element of L holds a | L = a * (1_. L)
let a be Element of L; :: thesis: a | L = a * (1_. L)

now :: thesis: for x being object st x in NAT holds
(a * (1_. L)) . x = (a | L) . x

let x be object ; :: thesis: ( x in NAT implies (a * (1_. L)) . b₁ = (a | L) . b₁ )
assume x in NAT ; :: thesis: (a * (1_. L)) . b₁ = (a | L) . b₁
then reconsider i = x as Element of NAT ;

per cases ( i = 0 or i > 0 ) ;

suppose A: i = 0 ; :: thesis: (a * (1_. L)) . b₁ = (a | L) . b₁

thus (a * (1_. L)) . x = a * ((1_. L) . i) by POLYNOM5:def 4
.= a * (1. L) by A, POLYNOM3:30
.= a
.= (a | L) . x by Th28, A ; :: thesis: verum

end;

suppose A: i > 0 ; :: thesis: (a * (1_. L)) . b₁ = (a | L) . b₁

thus (a * (1_. L)) . x = a * ((1_. L) . i) by POLYNOM5:def 4
.= a * (0. L) by A, POLYNOM3:30
.= (a | L) . x by Th28, A ; :: thesis: verum

end;

end;

end;

hence a | L = a * (1_. L) by FUNCT_2:12; :: thesis: verum