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%> . b1 = v * ((1_. L) . b1)
per cases ( n = 0 or n <> 0 ) ;
suppose A1: n = 0 ; :: thesis: <%v%> . b1 = v * ((1_. L) . b1)
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%> . b1 = v * ((1_. L) . b1)
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