let L be non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; :: thesis: for v being Element of L holds v * (1_. L) = <%v%>
let v be Element of L; :: thesis: v * (1_. L) = <%v%>

now :: thesis: for n being Element of NAT holds <%v%> . n = v * ((1_. L) . n)

let n be Element of NAT ; :: thesis: <%v%> . b₁ = v * ((1_. L) . b₁)

per cases ( n = 0 or n <> 0 ) ;

suppose A1: n = 0 ; :: thesis: <%v%> . b₁ = v * ((1_. L) . b₁)

hence <%v%> . n = v by ALGSEQ_1:def 5
.= v * (1. L)
.= v * ((1_. L) . n) by A1, POLYNOM3:30 ;
:: thesis: verum

end;

suppose A2: n <> 0 ; :: thesis: <%v%> . b₁ = v * ((1_. L) . b₁)

A3: len <%v%> <= 1 by ALGSEQ_1:def 5;
n >= 0 + 1 by A2, NAT_1:13;
hence <%v%> . n = 0. L by A3, ALGSEQ_1:8, XXREAL_0:2
.= v * (0. L)
.= v * ((1_. L) . n) by A2, POLYNOM3:30 ;
:: thesis: verum

end;

end;

end;

hence v * (1_. L) = <%v%> by Def4; :: thesis: verum